Theorems · Definition · functional analysis

LinearEquiv.toContinuousLinearEquivOfBounds

{𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [inst : Ring 𝕜] →
          [inst_1 : Ring 𝕜₂] →
            [inst_2 : SeminormedAddCommGroup E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : Module 𝕜 E] →
                  [inst_5 : Module 𝕜₂ F] →
                    {σ : 𝕜 →+* 𝕜₂} →
                      {σ₂₁ : 𝕜₂ →+* 𝕜} →
                        [inst_6 : RingHomInvPair σ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ] →
                            (e : E ≃ₛₗ[σ] F) →
                              (C_to C_inv : ℝ) →
                                (∀ (x : E), ‖e x‖ ≤ C_to * ‖x‖) → (∀ (x : F), ‖e.symm x‖ ≤ C_inv * ‖x‖) → E ≃SL[σ] F

Construct a continuous linear equivalence from a linear equivalence together with bounds in both directions.

Defined in

Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingRingSeminormedAddCommGroupSeminormedAddCommGroupModuleModuleRingHomInvPairRingHomInvPair