Theorems · Theorem · functional analysis

BoundedContinuousFunction.norm_eq

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ‖f‖ = sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C}

The norm of a bounded continuous function is the supremum of ‖f x‖. We use sInf to ensure that the definition works if α has no elements.

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Normed

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSeminormedAddCommGroup