Theorems · Theorem · functional analysis

LinearIsometryEquiv.enorm_toContinuousLinearMap

∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] [NontrivialTopology E] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_7 : RingHomInvPair σ₁₂ σ₂₁] [inst_8 : RingHomInvPair σ₂₁ σ₁₂] [inst_9 : RingHomIsometric σ₁₂]
  (e : E ≃ₛₗᵢ[σ₁₂] F), ‖↑↑e‖ₑ = 1

Defined in

Mathlib.Analysis.Normed.Operator.NormedSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNontriviallyNormedFieldNormedSpaceNormedSpaceNontrivialTopologyRingHomInvPairRingHomInvPairRingHomIsometric