Theorems · Definition · functional analysis

LinearIsometryEquiv.submoduleMap

{R : Type u_13} →
  {R₂ : Type u_15} →
    {M : Type u_16} →
      {M₂ : Type u_17} →
        [inst : Ring R] →
          [inst_1 : Ring R₂] →
            [inst_2 : SeminormedAddCommGroup M] →
              [inst_3 : SeminormedAddCommGroup M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                          {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                            (p : Submodule R M) → (e : M ≃ₛₗᵢ[σ₁₂] M₂) → ↥p ≃ₛₗᵢ[σ₁₂] ↥(Submodule.map (↑↑↑e) p)

A linear isometry equivalence between two modules restricts to a linear isometry equivalence from any submodule p of the domain onto the image of that submodule. This is a version of LinearEquiv.submoduleMap extended to linear isometry equivalences.

Defined in

Mathlib.Analysis.Normed.Operator.LinearIsometry

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingRingSeminormedAddCommGroupSeminormedAddCommGroupModuleModule