Theorems · Theorem · functional analysis

BoundedContinuousFunction.norm_lt_iff_of_compact

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [CompactSpace α]
  {f : BoundedContinuousFunction α β} {M : ℝ}, 0 < M → (‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M)

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Normed

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSeminormedAddCommGroupCompactSpace