Theorems · Theorem · functional analysis

BoundedContinuousFunction.norm_compContinuousCLM_le_one

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] {𝕜 : Type u_2}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 β] [inst_4 : SeminormedAddCommGroup γ] (g : C(γ, α)),
  ‖BoundedContinuousFunction.compContinuousCLM β 𝕜 g‖ ≤ 1

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Normed

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSeminormedAddCommGroupNontriviallyNormedFieldNormedSpaceSeminormedAddCommGroup