Theorems · Theorem · functional analysis

norm_lt_iff_of_compactlySupported

∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ]
  {f : BoundedContinuousFunction α γ}, f ∈ compactlySupported α γ → ∀ {M : ℝ}, 0 < M → (‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M)

Defined in

Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Cited by

1 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNonUnitalNormedRing