Theorems · Theorem · functional analysis

ContinuousAffineMap.decompLinearIsometryEquiv_symm_contLinear

∀ (𝕜 : Type u_1) (R : Type u_2) (V : Type u_3) (W : Type u_4) [inst : SeminormedAddCommGroup V]
  [inst_1 : SeminormedAddCommGroup W] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : Ring R] [inst_6 : Module R W] [inst_7 : ContinuousConstSMul R W]
  [inst_8 : SMulCommClass 𝕜 R W] (p : W × (V →L[𝕜] W)),
  ((ContinuousAffineMap.decompLinearIsometryEquiv 𝕜 R V W).symm p).contLinear = p.2

Defined in

Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNormedSpaceNormedSpaceRingModuleContinuousConstSMulSMulCommClass