mathlib documentation

analysis.normed_space.linear_isometry

(Semi-)linear isometries #

In this file we define linear_isometry σ₁₂ E E₂ (notation: E →ₛₗᵢ[σ₁₂] E₂) to be a semilinear isometric embedding of E into E₂ and linear_isometry_equiv (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 semi_normed_space and we specialize to normed_space when needed.

structure linear_isometry {R : Type u_1} {R₂ : Type u_2} [semiring R] [semiring R₂] (σ₁₂ : R →+* R₂) (E : Type u_10) (E₂ : Type u_11) [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
Type (max u_10 u_11)

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

@[instance]
def linear_isometry.has_coe_to_fun {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
has_coe_to_fun (E →ₛₗᵢ[σ₁₂] E₂) (λ (_x : E →ₛₗᵢ[σ₁₂] E₂), E → E₂)
Equations
@[simp]
theorem linear_isometry.coe_to_linear_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry.to_linear_map_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
theorem linear_isometry.coe_fn_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
function.injective (λ (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E), f x)
@[ext]
theorem linear_isometry.ext {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ (x : E), f x = g x) :
f = g
@[simp]
theorem linear_isometry.map_zero {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
f 0 = 0
@[simp]
theorem linear_isometry.map_add {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E) :
f (x + y) = f x + f y
@[simp]
theorem linear_isometry.map_sub {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E) :
f (x - y) = f x - f y
@[simp]
theorem linear_isometry.map_smulₛₗ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (c : R) (x : E) :
f (c x) = σ₁₂ c f x
@[simp]
theorem linear_isometry.map_smul {R : Type u_1} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R E₂] (f : E →ₗᵢ[R] E₂) (c : R) (x : E) :
f (c x) = c f x
@[simp]
theorem linear_isometry.norm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) :
@[simp]
theorem linear_isometry.nnnorm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) :
theorem linear_isometry.isometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry.dist_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E) :
dist (f x) (f y) = dist x y
@[simp]
theorem linear_isometry.edist_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E) :
edist (f x) (f y) = edist x y
theorem linear_isometry.injective {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E₂] [module R₂ E₂] [normed_group F] [module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry.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₂} [semi_normed_group E₂] [module R₂ E₂] [normed_group F] [module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) {x y : F} :
f₁ x = f₁ y x = y
theorem linear_isometry.map_ne {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E₂] [module R₂ E₂] [normed_group F] [module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) {x y : F} (h : x y) :
f₁ x f₁ y
theorem linear_isometry.lipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry.antilipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry.continuous {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry.ediam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (s : set E) :
theorem linear_isometry.ediam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry.diam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (s : set E) :
theorem linear_isometry.diam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
def linear_isometry.to_continuous_linear_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
E →SL[σ₁₂] E₂

Interpret a linear isometry as a continuous linear map.

Equations
@[simp]
theorem linear_isometry.coe_to_continuous_linear_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry.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₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) {α : Type u_3} [topological_space α] {g : α → E} :
def linear_isometry.id {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :

The identity linear isometry.

Equations
@[simp]
theorem linear_isometry.coe_id {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
@[simp]
theorem linear_isometry.id_apply {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] (x : E) :
@[instance]
def linear_isometry.inhabited {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
Equations
def linear_isometry.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₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [module R E] [module R₂ E₂] [module R₃ E₃] (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) :
E →ₛₗᵢ[σ₁₃] E₃

Composition of linear isometries.

Equations
@[simp]
theorem linear_isometry.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₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [module R E] [module R₂ E₂] [module R₃ E₃] (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) :
(g.comp f) = g f
@[simp]
theorem linear_isometry.id_comp {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry.comp_id {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry.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₄} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [semi_normed_group E₄] [module R E] [module R₂ E₂] [module R₃ E₃] [module R₄ E₄] (f : E₃ →ₛₗᵢ[σ₃₄] E₄) (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (h : E →ₛₗᵢ[σ₁₂] E₂) :
(f.comp g).comp h = f.comp (g.comp h)
@[instance]
def linear_isometry.monoid {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
Equations
@[simp]
theorem linear_isometry.coe_one {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
@[simp]
theorem linear_isometry.coe_mul {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] (f g : E →ₗᵢ[R] E) :
f * g = f g
def linear_map.to_linear_isometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) (hf : isometry f) :
E →ₛₗᵢ[σ₁₂] E₂

Construct a linear_isometry from a linear_map satisfying isometry.

Equations
def submodule.subtypeₗᵢ {E : Type u_5} [semi_normed_group E] {R' : Type u_10} [ring R'] [module R' E] (p : submodule R' E) :

submodule.subtype as a linear_isometry.

Equations
@[simp]
theorem submodule.coe_subtypeₗᵢ {E : Type u_5} [semi_normed_group E] {R' : Type u_10} [ring R'] [module R' E] (p : submodule R' E) :
@[simp]
theorem submodule.subtypeₗᵢ_to_linear_map {E : Type u_5} [semi_normed_group E] {R' : Type u_10} [ring R'] [module R' E] (p : submodule R' E) :
def submodule.subtypeL {E : Type u_5} [semi_normed_group E] {R' : Type u_10} [ring R'] [module R' E] (p : submodule R' E) :
p →L[R'] E

submodule.subtype as a continuous_linear_map.

Equations
@[simp]
theorem submodule.coe_subtypeL {E : Type u_5} [semi_normed_group E] {R' : Type u_10} [ring R'] [module R' E] (p : submodule R' E) :
@[simp]
theorem submodule.coe_subtypeL' {E : Type u_5} [semi_normed_group E] {R' : Type u_10} [ring R'] [module R' E] (p : submodule R' E) :
@[simp]
theorem submodule.range_subtypeL {E : Type u_5} [semi_normed_group E] {R' : Type u_10} [ring R'] [module R' E] (p : submodule R' E) :
@[simp]
theorem submodule.ker_subtypeL {E : Type u_5} [semi_normed_group E] {R' : Type u_10} [ring R'] [module R' E] (p : submodule R' E) :
structure linear_isometry_equiv {R : Type u_1} {R₂ : Type u_2} [semiring R] [semiring R₂] (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (E : Type u_10) (E₂ : Type u_11) [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
Type (max u_10 u_11)

A semilinear isometric equivalence between two normed vector spaces.

@[instance]
def linear_isometry_equiv.has_coe_to_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
has_coe_to_fun (E ≃ₛₗᵢ[σ₁₂] E₂) (λ (_x : E ≃ₛₗᵢ[σ₁₂] E₂), E → E₂)
Equations
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗ[σ₁₂] E₂) (he : ∀ (x : E), e x = x) :
@[simp]
theorem linear_isometry_equiv.coe_to_linear_equiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry_equiv.to_linear_equiv_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
@[ext]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] {e e' : E ≃ₛₗᵢ[σ₁₂] E₂} (h : ∀ (x : E), e x = e' x) :
e = e'
def linear_isometry_equiv.of_bounds {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗ[σ₁₂] E₂) (h₁ : ∀ (x : E), e x x) (h₂ : ∀ (y : E₂), (e.symm) y y) :
E ≃ₛₗᵢ[σ₁₂] E₂

Construct a linear_isometry_equiv from a linear_equiv and two inequalities: ∀ x, ∥e x∥ ≤ ∥x∥ and ∀ y, ∥e.symm y∥ ≤ ∥y∥.

Equations
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) :
def linear_isometry_equiv.to_linear_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E →ₛₗᵢ[σ₁₂] E₂

Reinterpret a linear_isometry_equiv as a linear_isometry.

Equations
@[simp]
theorem linear_isometry_equiv.coe_to_linear_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
def linear_isometry_equiv.to_isometric {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E ≃ᵢ E₂

Reinterpret a linear_isometry_equiv as an isometric.

Equations
@[simp]
theorem linear_isometry_equiv.coe_to_isometric {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
def linear_isometry_equiv.to_homeomorph {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E ≃ₜ E₂

Reinterpret a linear_isometry_equiv as an homeomorph.

Equations
@[simp]
theorem linear_isometry_equiv.coe_to_homeomorph {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry_equiv.continuous_at {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E} :
theorem linear_isometry_equiv.continuous_on {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {s : set E} :
theorem linear_isometry_equiv.continuous_within_at {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {s : set E} {x : E} :
def linear_isometry_equiv.to_continuous_linear_equiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E ≃SL[σ₁₂] E₂

Interpret a linear_isometry_equiv as a continuous linear equiv.

Equations
@[simp]
theorem linear_isometry_equiv.coe_to_continuous_linear_equiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
def linear_isometry_equiv.refl (R : Type u_1) (E : Type u_5) [semiring R] [semi_normed_group E] [module R E] :

Identity map as a linear_isometry_equiv.

Equations
@[instance]
def linear_isometry_equiv.inhabited {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
Equations
@[simp]
theorem linear_isometry_equiv.coe_refl {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
def linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E₂ ≃ₛₗᵢ[σ₂₁] E

The inverse linear_isometry_equiv.

Equations
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) :
e ((e.symm) x) = x
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) :
(e.symm) (e x) = x
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E} :
e x = 0 x = 0
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.symm.symm = e
@[simp]
theorem linear_isometry_equiv.to_linear_equiv_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.to_isometric_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.to_homeomorph_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
def linear_isometry_equiv.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₂} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃] [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [module R E] [module R₂ E₂] [module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
E ≃ₛₗᵢ[σ₁₃] E₃

Composition of linear_isometry_equivs as a linear_isometry_equiv.

Equations
@[simp]
theorem linear_isometry_equiv.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₂} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃] [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [module R E] [module R₂ E₂] [module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
(e₁.trans e₂) = e₂ e₁
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.symm_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.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₂} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃] [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [module R E] [module R₂ E₂] [module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
((e₁.trans e₂).symm) = (e₁.symm) (e₂.symm)
theorem linear_isometry_equiv.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₃} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃] [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃] [ring_hom_inv_pair σ₁₄ σ₄₁] [ring_hom_inv_pair σ₄₁ σ₁₄] [ring_hom_inv_pair σ₂₄ σ₄₂] [ring_hom_inv_pair σ₄₂ σ₂₄] [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] [ring_hom_comp_triple σ₄₂ σ₂₁ σ₄₁] [ring_hom_comp_triple σ₄₃ σ₃₂ σ₄₂] [ring_hom_comp_triple σ₄₃ σ₃₁ σ₄₁] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [semi_normed_group E₄] [module R E] [module R₂ E₂] [module R₃ E₃] [module R₄ E₄] (eEE₂ : E ≃ₛₗᵢ[σ₁₂] E₂) (eE₂E₃ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (eE₃E₄ : E₃ ≃ₛₗᵢ[σ₃₄] E₄) :
eEE₂.trans (eE₂E₃.trans eE₃E₄) = (eEE₂.trans eE₂E₃).trans eE₃E₄
@[instance]
def linear_isometry_equiv.group {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
Equations
@[simp]
theorem linear_isometry_equiv.coe_one {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
@[simp]
theorem linear_isometry_equiv.coe_mul {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] (e e' : E ≃ₗᵢ[R] E) :
e * e' = e e'
@[simp]
theorem linear_isometry_equiv.coe_inv {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] (e : E ≃ₗᵢ[R] E) :
@[instance]
def linear_isometry_equiv.continuous_linear_equiv.has_coe_t {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
has_coe_t (E ≃ₛₗᵢ[σ₁₂] E₂) (E ≃SL[σ₁₂] E₂)

Reinterpret a linear_isometry_equiv as a continuous_linear_equiv.

Equations
@[instance]
def linear_isometry_equiv.continuous_linear_map.has_coe_t {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
has_coe_t (E ≃ₛₗᵢ[σ₁₂] E₂) (E →SL[σ₁₂] E₂)
Equations
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e 0 = 0
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E) :
e (x + y) = e x + e y
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E) :
e (x - y) = e x - e y
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (c : R) (x : E) :
e (c x) = σ₁₂ c e x
@[simp]
theorem linear_isometry_equiv.map_smul {R : Type u_1} {E : Type u_5} {E₂ : Type u_6} [semiring R] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E) :
e (c x) = c e x
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E) :
dist (e x) (e y) = dist x y
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E) :
edist (e x) (e y) = edist x y
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x y : E} :
e x = e y x = y
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x y : E} (h : x y) :
e x e y
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : set E) :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : set E) :
@[simp]
theorem linear_isometry_equiv.comp_continuous_on_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {α : Type u_10} [topological_space α] {f : α → E} {s : set α} :
@[simp]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {α : Type u_10} [topological_space α] {f : α → E} :
def linear_isometry_equiv.of_surjective {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [semiring R] [semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E₂] [module R₂ E₂] [normed_group F] [module R F] (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : function.surjective f) :
F ≃ₛₗᵢ[σ₁₂] E₂

Construct a linear isometry equiv from a surjective linear isometry.

Equations
def linear_isometry_equiv.neg (R : Type u_1) {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :

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

Equations
@[simp]
theorem linear_isometry_equiv.coe_neg {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :