mem_compactlySupported — Mathlib

English

For f : α →ᵇ γ, f belongs to the compactly supported BC-functions if and only if HasCompactSupport f; i.e., membership in the ideal matches compact support.

Русский

Для f : α →ᵇ γ, f принадлежит к BC-функциям с компактной поддержкой тогда и только тогда, когда HasCompactSupport f.

LaTeX

$$$$f \in C_{cb}(\alpha, \gamma) \iff HasCompactSupport f.$$$$

Lean4

theorem mem_compactlySupported {f : α →ᵇ γ} : f ∈ C_cb(α, γ) ↔ HasCompactSupport f :=
  TwoSidedIdeal.mem_mk' {z : α →ᵇ γ | HasCompactSupport z} .zero .add .neg .mul_left .mul_right f

Похожие утверждения