compactlySupported — Mathlib

English

The two-sided ideal of compactly supported bounded continuous functions is closed under zero, addition, negation, and left/right multiplication by arbitrary bounded continuous functions.

Русский

Двусторонний идеал функций с компактной поддержкой замкнут относительно нулевой функции, сложения, взятия отрицания и левого/правого умножения на произвольные BC-функции.

LaTeX

$$$$\text{compactlySupported} = \.mk' \{z : α \to^b γ \;|\; \text{HasCompactSupport}(z)\} .zero .add .neg .mul_left .mul_right.$$$

Lean4

/-- The two-sided ideal of compactly supported functions. -/
def compactlySupported (α γ : Type*) [TopologicalSpace α] [NonUnitalNormedRing γ] : TwoSidedIdeal (α →ᵇ γ) :=
  .mk' {z | HasCompactSupport z} .zero .add .neg .mul_left .mul_right

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