Documentation

Mathlib.Analysis.NormedSpace.LinearIsometry

(Semi-)linear isometries #

In this file we define LinearIsometry σ₁₂ E E₂ (notation: E →ₛₗᵢ[σ₁₂] E₂) to be a semilinear isometric embedding of E into E₂ and LinearIsometryEquiv (notation: E ≃ₛₗᵢ[σ₁₂] E₂) to be a semilinear isometric equivalence between E and E₂. The notation for the associated purely linear concepts is E →ₗᵢ[R] E₂, E ≃ₗᵢ[R] E₂, and E →ₗᵢ⋆[R] E₂, E ≃ₗᵢ⋆[R] E₂ for the star-linear versions.

We also prove some trivial lemmas and provide convenience constructors.

Since a lot of elementary properties don't require ‖x‖ = 0 → x = 0 we start setting up the theory for SeminormedAddCommGroup and we specialize to NormedAddCommGroup when needed.

structure LinearIsometry {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] extends LinearMap :
Type (max u_11 u_12)

A σ₁₂-semilinear isometric embedding of a normed R-module into an R₂-module.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          class SemilinearIsometryClass (𝓕 : Type u_11) {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} [Semiring R] [Semiring R₂] (σ₁₂ : outParam (R →+* R₂)) (E : outParam (Type u_14)) (E₂ : outParam (Type u_15)) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] extends SemilinearMapClass :
          Type (max (max u_11 u_14) u_15)
          • coe : 𝓕EE₂
          • coe_injective' : Function.Injective FunLike.coe
          • map_add : ∀ (f : 𝓕) (x y : E), f (x + y) = f x + f y
          • map_smulₛₗ : ∀ (f : 𝓕) (r : R) (x : E), f (r x) = σ₁₂ r f x
          • norm_map : ∀ (f : 𝓕) (x : E), f x = x

          SemilinearIsometryClass F σ E E₂ asserts F is a type of bundled σ-semilinear isometries E → E₂.

          See also LinearIsometryClass F R E E₂ for the case where σ is the identity map on R.

          A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

          Instances
            @[inline, reducible]
            abbrev LinearIsometryClass (𝓕 : Type u_11) (R : outParam (Type u_12)) (E : outParam (Type u_13)) (E₂ : outParam (Type u_14)) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] :
            Type (max (max u_11 u_13) u_14)

            LinearIsometryClass F R E E₂ asserts F is a type of bundled R-linear isometries M → M₂.

            This is an abbreviation for SemilinearIsometryClass F (RingHom.id R) E E₂.

            Equations
            Instances For
              theorem SemilinearIsometryClass.isometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
              theorem SemilinearIsometryClass.continuous {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
              @[simp]
              theorem SemilinearIsometryClass.nnnorm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (x : E) :
              theorem SemilinearIsometryClass.lipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
              theorem SemilinearIsometryClass.antilipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
              theorem SemilinearIsometryClass.ediam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (s : Set E) :
              theorem SemilinearIsometryClass.ediam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
              theorem SemilinearIsometryClass.diam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (s : Set E) :
              theorem SemilinearIsometryClass.diam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
              Equations
              • One or more equations did not get rendered due to their size.
              theorem LinearIsometry.toLinearMap_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
              Function.Injective LinearIsometry.toLinearMap
              @[simp]
              theorem LinearIsometry.toLinearMap_inj {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E →ₛₗᵢ[σ₁₂] E₂} {g : E →ₛₗᵢ[σ₁₂] E₂} :
              f.toLinearMap = g.toLinearMap f = g
              instance LinearIsometry.instSemilinearIsometryClassLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
              SemilinearIsometryClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
              Equations
              @[simp]
              theorem LinearIsometry.coe_toLinearMap {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
              f.toLinearMap = f
              @[simp]
              theorem LinearIsometry.coe_mk {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) (hf : ∀ (x : E), f x = x) :
              { toLinearMap := f, norm_map' := hf } = f
              theorem LinearIsometry.coe_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
              Function.Injective fun f => f
              def LinearIsometry.Simps.apply {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E →ₛₗᵢ[σ₁₂] E₂) :
              EE₂

              See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

              Equations
              Instances For
                theorem LinearIsometry.ext {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E →ₛₗᵢ[σ₁₂] E₂} {g : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ (x : E), f x = g x) :
                f = g
                theorem LinearIsometry.congr_arg {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] {f : 𝓕} {x : E} {x' : E} :
                x = x'f x = f x'
                theorem LinearIsometry.congr_fun {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] {f : 𝓕} {g : 𝓕} (h : f = g) (x : E) :
                f x = g x
                theorem LinearIsometry.map_zero {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                f 0 = 0
                theorem LinearIsometry.map_add {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (y : E) :
                f (x + y) = f x + f y
                theorem LinearIsometry.map_neg {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) :
                f (-x) = -f x
                theorem LinearIsometry.map_sub {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (y : E) :
                f (x - y) = f x - f y
                theorem LinearIsometry.map_smulₛₗ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (c : R) (x : E) :
                f (c x) = σ₁₂ c f x
                theorem LinearIsometry.map_smul {R : Type u_1} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] (f : E →ₗᵢ[R] E₂) (c : R) (x : E) :
                f (c x) = c f x
                @[simp]
                theorem LinearIsometry.norm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) :
                f x = x
                theorem LinearIsometry.nnnorm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) :
                theorem LinearIsometry.isometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                @[simp]
                theorem LinearIsometry.isComplete_image_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) {s : Set E} :
                theorem LinearIsometry.isComplete_map_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) [RingHomSurjective σ₁₂] {p : Submodule R E} :
                IsComplete ↑(Submodule.map f.toLinearMap p) IsComplete p
                theorem LinearIsometry.isComplete_map_iff' {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) [RingHomSurjective σ₁₂] {p : Submodule R E} :
                instance LinearIsometry.completeSpace_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) [RingHomSurjective σ₁₂] (p : Submodule R E) [CompleteSpace { x // x p }] :
                Equations
                instance LinearIsometry.completeSpace_map' {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) [RingHomSurjective σ₁₂] (p : Submodule R E) [CompleteSpace { x // x p }] :
                CompleteSpace { x // x Submodule.map f.toLinearMap p }
                Equations
                @[simp]
                theorem LinearIsometry.dist_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (y : E) :
                dist (f x) (f y) = dist x y
                @[simp]
                theorem LinearIsometry.edist_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (y : E) :
                edist (f x) (f y) = edist x y
                theorem LinearIsometry.injective {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) :
                @[simp]
                theorem LinearIsometry.map_eq_iff {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) {x : F} {y : F} :
                f₁ x = f₁ y x = y
                theorem LinearIsometry.map_ne {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) {x : F} {y : F} (h : x y) :
                f₁ x f₁ y
                theorem LinearIsometry.lipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                theorem LinearIsometry.antilipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                theorem LinearIsometry.continuous {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                @[simp]
                theorem LinearIsometry.preimage_ball {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ) :
                f ⁻¹' Metric.ball (f x) r = Metric.ball x r
                @[simp]
                theorem LinearIsometry.preimage_sphere {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ) :
                f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
                @[simp]
                theorem LinearIsometry.preimage_closedBall {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ) :
                theorem LinearIsometry.ediam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
                theorem LinearIsometry.ediam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                theorem LinearIsometry.diam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
                theorem LinearIsometry.diam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                def LinearIsometry.toContinuousLinearMap {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                E →SL[σ₁₂] E₂

                Interpret a linear isometry as a continuous linear map.

                Equations
                Instances For
                  theorem LinearIsometry.toContinuousLinearMap_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
                  Function.Injective LinearIsometry.toContinuousLinearMap
                  @[simp]
                  theorem LinearIsometry.toContinuousLinearMap_inj {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E →ₛₗᵢ[σ₁₂] E₂} {g : E →ₛₗᵢ[σ₁₂] E₂} :
                  @[simp]
                  theorem LinearIsometry.coe_toContinuousLinearMap {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                  @[simp]
                  theorem LinearIsometry.comp_continuous_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) {α : Type u_11} [TopologicalSpace α] {g : αE} :
                  def LinearIsometry.id {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :

                  The identity linear isometry.

                  Equations
                  • LinearIsometry.id = { toLinearMap := LinearMap.id, norm_map' := (_ : ∀ (x : E), LinearMap.id x = LinearMap.id x) }
                  Instances For
                    @[simp]
                    theorem LinearIsometry.coe_id {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
                    LinearIsometry.id = id
                    @[simp]
                    theorem LinearIsometry.id_apply {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (x : E) :
                    LinearIsometry.id x = x
                    @[simp]
                    theorem LinearIsometry.id_toLinearMap {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
                    LinearIsometry.id.toLinearMap = LinearMap.id
                    Equations
                    • LinearIsometry.instInhabitedLinearIsometryIdToNonAssocSemiring = { default := LinearIsometry.id }
                    def LinearIsometry.comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) :
                    E →ₛₗᵢ[σ₁₃] E₃

                    Composition of linear isometries.

                    Equations
                    Instances For
                      @[simp]
                      theorem LinearIsometry.coe_comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) :
                      ↑(LinearIsometry.comp g f) = g f
                      @[simp]
                      theorem LinearIsometry.id_comp {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                      LinearIsometry.comp LinearIsometry.id f = f
                      @[simp]
                      theorem LinearIsometry.comp_id {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
                      LinearIsometry.comp f LinearIsometry.id = f
                      theorem LinearIsometry.comp_assoc {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {R₄ : Type u_4} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} {E₄ : Type u_8} [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₄] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [SeminormedAddCommGroup E₄] [Module R E] [Module R₂ E₂] [Module R₃ E₃] [Module R₄ E₄] (f : E₃ →ₛₗᵢ[σ₃₄] E₄) (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (h : E →ₛₗᵢ[σ₁₂] E₂) :
                      Equations
                      • One or more equations did not get rendered due to their size.
                      @[simp]
                      theorem LinearIsometry.coe_one {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
                      1 = id
                      @[simp]
                      theorem LinearIsometry.coe_mul {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (f : E →ₗᵢ[R] E) (g : E →ₗᵢ[R] E) :
                      ↑(f * g) = f g
                      theorem LinearIsometry.one_def {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
                      1 = LinearIsometry.id
                      theorem LinearIsometry.mul_def {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (f : E →ₗᵢ[R] E) (g : E →ₗᵢ[R] E) :
                      theorem LinearIsometry.coe_pow {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (f : E →ₗᵢ[R] E) (n : ) :
                      ↑(f ^ n) = (f)^[n]
                      def LinearMap.toLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) (hf : Isometry f) :
                      E →ₛₗᵢ[σ₁₂] E₂

                      Construct a LinearIsometry from a LinearMap satisfying Isometry.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Submodule.subtypeₗᵢ {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_11} [Ring R'] [Module R' E] (p : Submodule R' E) :
                        { x // x p } →ₗᵢ[R'] E

                        Submodule.subtype as a LinearIsometry.

                        Equations
                        Instances For
                          @[simp]
                          theorem Submodule.coe_subtypeₗᵢ {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_11} [Ring R'] [Module R' E] (p : Submodule R' E) :
                          @[simp]
                          theorem Submodule.subtypeₗᵢ_toLinearMap {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_11} [Ring R'] [Module R' E] (p : Submodule R' E) :
                          structure LinearIsometryEquiv {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] extends LinearEquiv :
                          Type (max u_11 u_12)

                          A semilinear isometric equivalence between two normed vector spaces.

                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  class SemilinearIsometryEquivClass (𝓕 : Type u_11) {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} [Semiring R] [Semiring R₂] (σ₁₂ : outParam (R →+* R₂)) {σ₂₁ : outParam (R₂ →+* R)} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E : outParam (Type u_14)) (E₂ : outParam (Type u_15)) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] extends SemilinearEquivClass :
                                  Type (max (max u_11 u_14) u_15)

                                  SemilinearIsometryEquivClass F σ E E₂ asserts F is a type of bundled σ-semilinear isometric equivs E → E₂.

                                  See also LinearIsometryEquivClass F R E E₂ for the case where σ is the identity map on R.

                                  A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

                                  Instances
                                    @[inline, reducible]
                                    abbrev LinearIsometryEquivClass (𝓕 : Type u_11) (R : outParam (Type u_12)) (E : outParam (Type u_13)) (E₂ : outParam (Type u_14)) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] :
                                    Type (max (max u_11 u_13) u_14)

                                    LinearIsometryEquivClass F R E E₂ asserts F is a type of bundled R-linear isometries M → M₂.

                                    This is an abbreviation for SemilinearIsometryEquivClass F (RingHom.id R) E E₂.

                                    Equations
                                    Instances For
                                      instance SemilinearIsometryEquivClass.instSemilinearIsometryClass {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} (𝓕 : Type u_10) [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [s : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂] :
                                      SemilinearIsometryClass 𝓕 σ₁₂ E E₂
                                      Equations
                                      theorem LinearIsometryEquiv.toLinearEquiv_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
                                      Function.Injective LinearIsometryEquiv.toLinearEquiv
                                      @[simp]
                                      theorem LinearIsometryEquiv.toLinearEquiv_inj {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E ≃ₛₗᵢ[σ₁₂] E₂} {g : E ≃ₛₗᵢ[σ₁₂] E₂} :
                                      f.toLinearEquiv = g.toLinearEquiv f = g
                                      instance LinearIsometryEquiv.instSemilinearIsometryEquivClassLinearIsometryEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
                                      SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
                                      Equations
                                      instance LinearIsometryEquiv.instCoeFunLinearIsometryEquivForAll {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
                                      CoeFun (E ≃ₛₗᵢ[σ₁₂] E₂) fun x => EE₂

                                      Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun directly.

                                      Equations
                                      • LinearIsometryEquiv.instCoeFunLinearIsometryEquivForAll = { coe := FunLike.coe }
                                      theorem LinearIsometryEquiv.coe_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
                                      Function.Injective FunLike.coe
                                      @[simp]
                                      theorem LinearIsometryEquiv.coe_mk {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗ[σ₁₂] E₂) (he : ∀ (x : E), e x = x) :
                                      { toLinearEquiv := e, norm_map' := he } = e
                                      @[simp]
                                      theorem LinearIsometryEquiv.coe_toLinearEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                      e.toLinearEquiv = e
                                      theorem LinearIsometryEquiv.ext {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {e : E ≃ₛₗᵢ[σ₁₂] E₂} {e' : E ≃ₛₗᵢ[σ₁₂] E₂} (h : ∀ (x : E), e x = e' x) :
                                      e = e'
                                      theorem LinearIsometryEquiv.congr_arg {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E ≃ₛₗᵢ[σ₁₂] E₂} {x : E} {x' : E} :
                                      x = x'f x = f x'
                                      theorem LinearIsometryEquiv.congr_fun {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E ≃ₛₗᵢ[σ₁₂] E₂} {g : E ≃ₛₗᵢ[σ₁₂] E₂} (h : f = g) (x : E) :
                                      f x = g x
                                      def LinearIsometryEquiv.ofBounds {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗ[σ₁₂] E₂) (h₁ : ∀ (x : E), e x x) (h₂ : ∀ (y : E₂), ↑(LinearEquiv.symm e) y y) :
                                      E ≃ₛₗᵢ[σ₁₂] E₂

                                      Construct a LinearIsometryEquiv from a LinearEquiv and two inequalities: ∀ x, ‖e x‖ ≤ ‖x‖ and ∀ y, ‖e.symm y‖ ≤ ‖y‖.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem LinearIsometryEquiv.norm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) :
                                        e x = x
                                        def LinearIsometryEquiv.toLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                        E →ₛₗᵢ[σ₁₂] E₂

                                        Reinterpret a LinearIsometryEquiv as a LinearIsometry.

                                        Equations
                                        Instances For
                                          theorem LinearIsometryEquiv.toLinearIsometry_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
                                          Function.Injective LinearIsometryEquiv.toLinearIsometry
                                          @[simp]
                                          theorem LinearIsometryEquiv.toLinearIsometry_inj {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E ≃ₛₗᵢ[σ₁₂] E₂} {g : E ≃ₛₗᵢ[σ₁₂] E₂} :
                                          @[simp]
                                          theorem LinearIsometryEquiv.coe_toLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                          theorem LinearIsometryEquiv.isometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                          def LinearIsometryEquiv.toIsometryEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                          E ≃ᵢ E₂

                                          Reinterpret a LinearIsometryEquiv as an IsometryEquiv.

                                          Equations
                                          Instances For
                                            theorem LinearIsometryEquiv.toIsometryEquiv_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
                                            Function.Injective LinearIsometryEquiv.toIsometryEquiv
                                            @[simp]
                                            theorem LinearIsometryEquiv.toIsometryEquiv_inj {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E ≃ₛₗᵢ[σ₁₂] E₂} {g : E ≃ₛₗᵢ[σ₁₂] E₂} :
                                            @[simp]
                                            theorem LinearIsometryEquiv.coe_toIsometryEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                            theorem LinearIsometryEquiv.range_eq_univ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                            Set.range e = Set.univ
                                            def LinearIsometryEquiv.toHomeomorph {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                            E ≃ₜ E₂

                                            Reinterpret a LinearIsometryEquiv as a Homeomorph.

                                            Equations
                                            Instances For
                                              theorem LinearIsometryEquiv.toHomeomorph_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
                                              Function.Injective LinearIsometryEquiv.toHomeomorph
                                              @[simp]
                                              theorem LinearIsometryEquiv.toHomeomorph_inj {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E ≃ₛₗᵢ[σ₁₂] E₂} {g : E ≃ₛₗᵢ[σ₁₂] E₂} :
                                              @[simp]
                                              theorem LinearIsometryEquiv.coe_toHomeomorph {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                              theorem LinearIsometryEquiv.continuous {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                              theorem LinearIsometryEquiv.continuousAt {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E} :
                                              ContinuousAt (e) x
                                              theorem LinearIsometryEquiv.continuousOn {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {s : Set E} :
                                              ContinuousOn (e) s
                                              theorem LinearIsometryEquiv.continuousWithinAt {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {s : Set E} {x : E} :
                                              def LinearIsometryEquiv.toContinuousLinearEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                              E ≃SL[σ₁₂] E₂

                                              Interpret a LinearIsometryEquiv as a ContinuousLinearEquiv.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem LinearIsometryEquiv.toContinuousLinearEquiv_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
                                                Function.Injective LinearIsometryEquiv.toContinuousLinearEquiv
                                                @[simp]
                                                theorem LinearIsometryEquiv.toContinuousLinearEquiv_inj {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E ≃ₛₗᵢ[σ₁₂] E₂} {g : E ≃ₛₗᵢ[σ₁₂] E₂} :
                                                @[simp]
                                                theorem LinearIsometryEquiv.coe_toContinuousLinearEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :

                                                Identity map as a LinearIsometryEquiv.

                                                Equations
                                                Instances For

                                                  Linear isometry equiv between a space and its lift to another universe.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    Equations
                                                    @[simp]
                                                    def LinearIsometryEquiv.symm {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                    E₂ ≃ₛₗᵢ[σ₂₁] E

                                                    The inverse LinearIsometryEquiv.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem LinearIsometryEquiv.apply_symm_apply {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) :
                                                      e (↑(LinearIsometryEquiv.symm e) x) = x
                                                      @[simp]
                                                      theorem LinearIsometryEquiv.symm_apply_apply {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) :
                                                      ↑(LinearIsometryEquiv.symm e) (e x) = x
                                                      theorem LinearIsometryEquiv.map_eq_zero_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E} :
                                                      e x = 0 x = 0
                                                      @[simp]
                                                      theorem LinearIsometryEquiv.symm_symm {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                      @[simp]
                                                      theorem LinearIsometryEquiv.toLinearEquiv_symm {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                      LinearEquiv.symm e.toLinearEquiv = (LinearIsometryEquiv.symm e).toLinearEquiv
                                                      @[simp]
                                                      theorem LinearIsometryEquiv.toIsometryEquiv_symm {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                      @[simp]
                                                      theorem LinearIsometryEquiv.toHomeomorph_symm {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                      def LinearIsometryEquiv.Simps.apply {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                      EE₂

                                                      See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

                                                      Equations
                                                      Instances For
                                                        def LinearIsometryEquiv.Simps.symm_apply {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                        E₂E

                                                        See Note [custom simps projection]

                                                        Equations
                                                        Instances For
                                                          def LinearIsometryEquiv.trans {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
                                                          E ≃ₛₗᵢ[σ₁₃] E₃

                                                          Composition of LinearIsometryEquivs as a LinearIsometryEquiv.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.coe_trans {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
                                                            ↑(LinearIsometryEquiv.trans e₁ e₂) = e₂ e₁
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.trans_apply {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (c : E) :
                                                            ↑(LinearIsometryEquiv.trans e₁ e₂) c = e₂ (e₁ c)
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.toLinearEquiv_trans {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
                                                            (LinearIsometryEquiv.trans e e').toLinearEquiv = LinearEquiv.trans e.toLinearEquiv e'.toLinearEquiv
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.trans_refl {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.refl_trans {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.self_trans_symm {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.symm_trans_self {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.symm_comp_self {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.self_comp_symm {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.symm_trans {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
                                                            theorem LinearIsometryEquiv.coe_symm_trans {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
                                                            theorem LinearIsometryEquiv.trans_assoc {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {R₄ : Type u_4} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} {E₄ : Type u_8} [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₄] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₁₄ : R →+* R₄} {σ₄₁ : R₄ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₂₄ : R₂ →+* R₄} {σ₄₂ : R₄ →+* R₂} {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomInvPair σ₁₄ σ₄₁] [RingHomInvPair σ₄₁ σ₁₄] [RingHomInvPair σ₂₄ σ₄₂] [RingHomInvPair σ₄₂ σ₂₄] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₄₂ σ₂₁ σ₄₁] [RingHomCompTriple σ₄₃ σ₃₂ σ₄₂] [RingHomCompTriple σ₄₃ σ₃₁ σ₄₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [SeminormedAddCommGroup E₄] [Module R E] [Module R₂ E₂] [Module R₃ E₃] [Module R₄ E₄] (eEE₂ : E ≃ₛₗᵢ[σ₁₂] E₂) (eE₂E₃ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (eE₃E₄ : E₃ ≃ₛₗᵢ[σ₃₄] E₄) :
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.coe_one {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
                                                            1 = id
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.coe_mul {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (e : E ≃ₗᵢ[R] E) (e' : E ≃ₗᵢ[R] E) :
                                                            ↑(e * e') = e e'
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.mul_def {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (e : E ≃ₗᵢ[R] E) (e' : E ≃ₗᵢ[R] E) :

                                                            Lemmas about mixing the group structure with definitions. Because we have multiple ways to express LinearIsometryEquiv.refl, LinearIsometryEquiv.symm, and LinearIsometryEquiv.trans, we want simp lemmas for every combination. The assumption made here is that if you're using the group structure, you want to preserve it after simp.

                                                            This copies the approach used by the lemmas near Equiv.Perm.trans_one.

                                                            @[simp]
                                                            theorem LinearIsometryEquiv.trans_one {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.one_trans {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            @[simp]
                                                            @[simp]

                                                            Reinterpret a LinearIsometryEquiv as a ContinuousLinearEquiv.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.coe_coe {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            ↑(ContinuousLinearEquiv.mk e.toLinearEquiv) = e
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.coe_coe'' {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            ↑(ContinuousLinearEquiv.mk e.toLinearEquiv) = e
                                                            theorem LinearIsometryEquiv.map_zero {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            e 0 = 0
                                                            theorem LinearIsometryEquiv.map_add {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (y : E) :
                                                            e (x + y) = e x + e y
                                                            theorem LinearIsometryEquiv.map_sub {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (y : E) :
                                                            e (x - y) = e x - e y
                                                            theorem LinearIsometryEquiv.map_smulₛₗ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (c : R) (x : E) :
                                                            e (c x) = σ₁₂ c e x
                                                            theorem LinearIsometryEquiv.map_smul {R : Type u_1} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E) :
                                                            e (c x) = c e x
                                                            theorem LinearIsometryEquiv.nnnorm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.dist_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (y : E) :
                                                            dist (e x) (e y) = dist x y
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.edist_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (y : E) :
                                                            edist (e x) (e y) = edist x y
                                                            theorem LinearIsometryEquiv.bijective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            theorem LinearIsometryEquiv.injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            theorem LinearIsometryEquiv.surjective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            theorem LinearIsometryEquiv.map_eq_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E} {y : E} :
                                                            e x = e y x = y
                                                            theorem LinearIsometryEquiv.map_ne {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E} {y : E} (h : x y) :
                                                            e x e y
                                                            theorem LinearIsometryEquiv.lipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            theorem LinearIsometryEquiv.antilipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
                                                            theorem LinearIsometryEquiv.image_eq_preimage {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.ediam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.diam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.preimage_ball {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) (r : ) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.preimage_sphere {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) (r : ) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.preimage_closedBall {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) (r : ) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.image_ball {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ) :
                                                            e '' Metric.ball x r = Metric.ball (e x) r
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.image_sphere {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ) :
                                                            e '' Metric.sphere x r = Metric.sphere (e x) r
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.image_closedBall {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ) :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.comp_continuousOn_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {α : Type u_11} [TopologicalSpace α] {f : αE} {s : Set α} :
                                                            @[simp]
                                                            theorem LinearIsometryEquiv.comp_continuous_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {α : Type u_11} [TopologicalSpace α] {f : αE} :
                                                            instance LinearIsometryEquiv.completeSpace_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (p : Submodule R E) [CompleteSpace { x // x p }] :
                                                            CompleteSpace { x // x Submodule.map (e.toLinearEquiv) p }
                                                            Equations
                                                            noncomputable def LinearIsometryEquiv.ofSurjective {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective f) :
                                                            F ≃ₛₗᵢ[σ₁₂] E₂

                                                            Construct a linear isometry equiv from a surjective linear isometry.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[simp]
                                                              theorem LinearIsometryEquiv.coe_ofSurjective {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective f) :
                                                              def LinearIsometryEquiv.ofLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : LinearMap.comp f.toLinearMap g = LinearMap.id) (h₂ : LinearMap.comp g f.toLinearMap = LinearMap.id) :
                                                              E ≃ₛₗᵢ[σ₁₂] E₂

                                                              If a linear isometry has an inverse, it is a linear isometric equivalence.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[simp]
                                                                theorem LinearIsometryEquiv.coe_ofLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : LinearMap.comp f.toLinearMap g = LinearMap.id) (h₂ : LinearMap.comp g f.toLinearMap = LinearMap.id) :
                                                                ↑(LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂) = f
                                                                @[simp]
                                                                theorem LinearIsometryEquiv.coe_ofLinearIsometry_symm {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : LinearMap.comp f.toLinearMap g = LinearMap.id) (h₂ : LinearMap.comp g f.toLinearMap = LinearMap.id) :

                                                                The negation operation on a normed space E, considered as a linear isometry equivalence.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  @[simp]
                                                                  theorem LinearIsometryEquiv.coe_neg {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
                                                                  ↑(LinearIsometryEquiv.neg R) = fun x => -x
                                                                  def LinearIsometryEquiv.prodAssoc (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R E₂] [Module R E₃] :
                                                                  (E × E₂) × E₃ ≃ₗᵢ[R] E × E₂ × E₃

                                                                  The natural equivalence (E × E₂) × E₃ ≃ E × (E₂ × E₃) is a linear isometry.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem LinearIsometryEquiv.coe_prodAssoc (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R E₂] [Module R E₃] :
                                                                    ↑(LinearIsometryEquiv.prodAssoc R E E₂ E₃) = ↑(Equiv.prodAssoc E E₂ E₃)
                                                                    @[simp]
                                                                    theorem LinearIsometryEquiv.coe_prodAssoc_symm (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R E₂] [Module R E₃] :
                                                                    ↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.prodAssoc R E E₂ E₃)) = (Equiv.prodAssoc E E₂ E₃).symm
                                                                    @[simp]
                                                                    theorem LinearIsometryEquiv.ofTop_apply (E : Type u_5) [SeminormedAddCommGroup E] {R : Type u_12} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ) (self : { x // x p }) :
                                                                    ↑(LinearIsometryEquiv.ofTop E p hp) self = self
                                                                    @[simp]
                                                                    theorem LinearIsometryEquiv.ofTop_toLinearEquiv (E : Type u_5) [SeminormedAddCommGroup E] {R : Type u_12} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ) :
                                                                    (LinearIsometryEquiv.ofTop E p hp).toLinearEquiv = LinearEquiv.ofTop p hp
                                                                    @[simp]
                                                                    theorem LinearIsometryEquiv.ofTop_symm_apply_coe (E : Type u_5) [SeminormedAddCommGroup E] {R : Type u_12} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ) (x : E) :
                                                                    def LinearIsometryEquiv.ofTop (E : Type u_5) [SeminormedAddCommGroup E] {R : Type u_12} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ) :
                                                                    { x // x p } ≃ₗᵢ[R] E

                                                                    If p is a submodule that is equal to , then LinearIsometryEquiv.ofTop p hp is the "identity" equivalence between p and E.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      def LinearIsometryEquiv.ofEq {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_12} [Ring R'] [Module R' E] (p : Submodule R' E) (q : Submodule R' E) (hpq : p = q) :
                                                                      { x // x p } ≃ₗᵢ[R'] { x // x q }

                                                                      LinearEquiv.ofEq as a LinearIsometryEquiv.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem LinearIsometryEquiv.coe_ofEq_apply {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_12} [Ring R'] [Module R' E] {p : Submodule R' E} {q : Submodule R' E} (h : p = q) (x : { x // x p }) :
                                                                        ↑(↑(LinearIsometryEquiv.ofEq p q h) x) = x
                                                                        @[simp]
                                                                        theorem LinearIsometryEquiv.ofEq_symm {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_12} [Ring R'] [Module R' E] {p : Submodule R' E} {q : Submodule R' E} (h : p = q) :
                                                                        @[simp]
                                                                        theorem LinearIsometryEquiv.ofEq_rfl {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_12} [Ring R'] [Module R' E] {p : Submodule R' E} :
                                                                        theorem Basis.ext_linearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {ι : Type u_11} (b : Basis ι R E) {f₁ : E →ₛₗᵢ[σ₁₂] E₂} {f₂ : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ (i : ι), f₁ (b i) = f₂ (b i)) :
                                                                        f₁ = f₂

                                                                        Two linear isometries are equal if they are equal on basis vectors.

                                                                        theorem Basis.ext_linearIsometryEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {ι : Type u_11} (b : Basis ι R E) {f₁ : E ≃ₛₗᵢ[σ₁₂] E₂} {f₂ : E ≃ₛₗᵢ[σ₁₂] E₂} (h : ∀ (i : ι), f₁ (b i) = f₂ (b i)) :
                                                                        f₁ = f₂

                                                                        Two linear isometric equivalences are equal if they are equal on basis vectors.

                                                                        @[simp]
                                                                        theorem LinearIsometry.equivRange_apply_coe {E : Type u_5} {F : Type u_9} [SeminormedAddCommGroup E] [NormedAddCommGroup F] {R : Type u_11} {S : Type u_12} [Semiring R] [Ring S] [Module S E] [Module R F] {σ₁₂ : R →+* S} {σ₂₁ : S →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : F →ₛₗᵢ[σ₁₂] E) (a : F) :
                                                                        ↑(↑(LinearIsometry.equivRange f) a) = f a
                                                                        noncomputable def LinearIsometry.equivRange {E : Type u_5} {F : Type u_9} [SeminormedAddCommGroup E] [NormedAddCommGroup F] {R : Type u_11} {S : Type u_12} [Semiring R] [Ring S] [Module S E] [Module R F] {σ₁₂ : R →+* S} {σ₂₁ : S →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : F →ₛₗᵢ[σ₁₂] E) :
                                                                        F ≃ₛₗᵢ[σ₁₂] { x // x LinearMap.range f.toLinearMap }

                                                                        Reinterpret a LinearIsometry as a LinearIsometryEquiv to the range.

                                                                        Equations
                                                                        Instances For