Theorems · Theorem · general topology

ContinuousMap.nnnorm_smul_const

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] {R : Type u_4} {β : Type u_5}
  [inst_2 : SeminormedAddCommGroup β] [inst_3 : SeminormedRing R] [inst_4 : Module R β] [inst_5 : NormSMulClass R β]
  (f : C(α, R)) (b : β), ‖f • ContinuousMap.const α b‖₊ = ‖f‖₊ * ‖b‖₊

Defined in

Mathlib.Topology.ContinuousMap.Compact

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCompactSpaceSeminormedAddCommGroupSeminormedRingModuleNormSMulClass