Theorems · Theorem · functional analysis

ContinuousLinearMap.nnnorm_id

∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] [NontrivialTopology E], ‖ContinuousLinearMap.id 𝕜 E‖₊ = 1

If a normed space is (topologically) non-trivial, then the norm of the identity equals 1.

Defined in

Mathlib.Analysis.Normed.Operator.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNontriviallyNormedFieldNormedSpaceNontrivialTopology