Theorems · Theorem · functional analysis

ContinuousLinearMap.norm_single

∀ {ι : Type u_9} [inst : Fintype ι] [inst_1 : DecidableEq ι] (𝕜 : Type u_10) [inst_2 : NontriviallyNormedField 𝕜]
  (E : ι → Type u_11) [inst_3 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] (i : ι)
  [NontrivialTopology (E i)], ‖ContinuousLinearMap.single 𝕜 E i‖ = 1

Defined in

Mathlib.Analysis.Normed.Operator.NormedSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqNontriviallyNormedFieldSeminormedAddCommGroupNormedSpaceNontrivialTopology