Theorems · Theorem · functional analysis

SemilinearIsometryClass.norm_map

∀ {𝓕 : Type u_11} {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} {inst : Semiring R} {inst_1 : Semiring R₂}
  {σ₁₂ : outParam (R →+* R₂)} {E : outParam (Type u_14)} {E₂ : outParam (Type u_15)} {inst_2 : SeminormedAddCommGroup E}
  {inst_3 : SeminormedAddCommGroup E₂} {inst_4 : Module R E} {inst_5 : Module R₂ E₂} {inst_6 : FunLike 𝓕 E E₂}
  [self : SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (x : E), ‖f x‖ = ‖x‖

Defined in

Mathlib.Analysis.Normed.Operator.LinearIsometry

Cited by

2 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

SemilinearIsometryClass