Compactly supported bounded continuous functions

The two-sided ideal of compactly supported bounded continuous functions taking values in a metric space, with the uniform distance.

def compactlySupported (α : Type u_1) (γ : Type u_2) [TopologicalSpace α] [NonUnitalNormedRing γ] : TwoSidedIdeal (BoundedContinuousFunction α γ)

The two-sided ideal of compactly supported functions.

def BoundedContinuousFunction.«termC_cb(_,_)» : Lean.ParserDescr

The two-sided ideal of compactly supported functions.

theorem mem_compactlySupported {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] {f : BoundedContinuousFunction α γ} : f ∈ compactlySupported α γ ↔ HasCompactSupport ⇑f

theorem exist_norm_eq {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] [c : Nonempty α] {f : BoundedContinuousFunction α γ} (h : f ∈ compactlySupported α γ) : ∃ (x : α), ‖f x‖ = ‖f‖

theorem norm_lt_iff_of_compactlySupported {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] {f : BoundedContinuousFunction α γ} (h : f ∈ compactlySupported α γ) {M : ℝ} (M0 : 0 < M) : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem norm_lt_iff_of_nonempty_compactlySupported {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] [c : Nonempty α] {f : BoundedContinuousFunction α γ} (h : f ∈ compactlySupported α γ) {M : ℝ} : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem compactlySupported_eq_top_of_isCompact {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] (h : IsCompact Set.univ) : compactlySupported α γ = ⊤

theorem compactlySupported_eq_top {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] [CompactSpace α] : compactlySupported α γ = ⊤

theorem compactlySupported_eq_top_iff {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] [Nontrivial γ] : compactlySupported α γ = ⊤ ↔ IsCompact Set.univ

def ofCompactSupport {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] (g : α → γ) (hg₁ : Continuous g) (hg₂ : HasCompactSupport g) : BoundedContinuousFunction α γ

A compactly supported continuous function is automatically bounded. This constructor gives an object of α →ᵇ γ from g : α → γ and these assumptions.

theorem ofCompactSupport_mem {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] (g : α → γ) (hg₁ : Continuous g) (hg₂ : HasCompactSupport g) : ofCompactSupport g hg₁ hg₂ ∈ compactlySupported α γ

instance instSMulContinuousMapSubtypeBoundedContinuousFunctionMemTwoSidedIdealCompactlySupported {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] : SMul C(α, γ) ↥(compactlySupported α γ)