Theorems · Theorem · functional analysis

LinearEquiv.extendOfIsometry_symm_eq

∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : NormedField 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] [inst_6 : NormedAddCommGroup Eₗ] [inst_7 : NormedSpace 𝕜 Eₗ] [inst_8 : CompleteSpace Eₗ]
  [inst_9 : NormedAddCommGroup Fₗ] [inst_10 : NormedSpace 𝕜₂ Fₗ] [inst_11 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_12 : RingHomInvPair σ₁₂ σ₂₁] [inst_13 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂)
  (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (x : F),
  (f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm).symm (e₂ x) = e₁ (f.symm x)

Defined in

Mathlib.Analysis.Normed.Operator.Extend

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedFieldAddCommGroupModuleAddCommGroupModuleNormedAddCommGroupNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceCompleteSpaceRingHomInvPairRingHomInvPair