Theorems · Theorem · functional analysis

NormedAddGroupHom.norm_id_le

∀ (V : Type u_1) [inst : SeminormedAddCommGroup V], ‖NormedAddGroupHom.id V‖ ≤ 1

The norm of the identity is at most 1. It is in fact 1, except when the norm of every element vanishes, where it is 0. (Since we are working with seminorms this can happen even if the space is non-trivial.) It means that one cannot do better than an inequality in general.

Defined in

Mathlib.Analysis.Normed.Group.Hom

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroup