Theorems · Theorem · functional analysis

ContinuousLinearMap.norm_id_le

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

The norm of the identity is at most 1. It is in fact 1, except when the space is trivial where it is 0. It means that one cannot do better than an inequality in general.

Defined in

Mathlib.Analysis.Normed.Operator.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNontriviallyNormedFieldNormedSpace