Mathlib Map

Theorems · Theorem · functional analysis

BoundedContinuousFunction.norm_const_eq

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [h : Nonempty α] (b : β),
  ‖BoundedContinuousFunction.const α b‖ = ‖b‖
Defined in
Mathlib.Topology.ContinuousMap.Bounded.Normed
Cited by
1 results in Mathlib
Foundations
Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceSeminormedAddCommGroupNonempty
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

BoundedContinuousFunction.nnnorm_const_eq · cited by 0BoundedContinuousFunction…Real · cited by 25697RealTopologicalSpace · cited by 24529TopologicalSpaceNorm.norm · cited by 5413Norm.normSeminormedAddCommGroup · cited by 2671SeminormedAddCommGrouple_antisymm · cited by 2068le_antisymmBoundedContinuousFunction · cited by 511BoundedContinuousFunctionBoundedContinuousFunction.norm_coe_le_norm · cited by 25BoundedContinuousFunction…BoundedContinuousFunction.const · cited by 20BoundedContinuousFunction…BoundedContinuousFunction.norm_const_le · cited by 2BoundedContinuousFunction…BoundedContinuousFunction.nor…CITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.