Theorems · Definition · functional analysis

LinearIsometry.submoduleMap

{R : Type u_11} →
  {M : Type u_14} →
    {M₁ : Type u_15} →
      [inst : Ring R] →
        [inst_1 : SeminormedAddCommGroup M] →
          [inst_2 : SeminormedAddCommGroup M₁] →
            [inst_3 : Module R M] →
              [inst_4 : Module R M₁] → (p : Submodule R M) → (e : M →ₗᵢ[R] M₁) → ↥p →ₗᵢ[R] ↥(Submodule.map (↑e) p)

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

Defined in

Mathlib.Analysis.Normed.Operator.LinearIsometry

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingSeminormedAddCommGroupSeminormedAddCommGroupModuleModule