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_group and we specialize to normed_group 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.

Instances for linear_isometry
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₂] :
@[simp]
theorem linear_isometry.to_linear_map_inj {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₂} :
@[protected, instance]
def linear_isometry.add_monoid_hom_class {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₂] :
add_monoid_hom_class (E →ₛₗᵢ[σ₁₂] E₂) E E₂
Equations
@[protected, 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₂)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

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₂) :
@[simp]
theorem linear_isometry.coe_mk {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 : ∀ (x : E), f x = x) :
theorem linear_isometry.coe_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₂] :
@[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
@[protected]
theorem linear_isometry.congr_arg {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 x' : E} :
x = x'f x = f x'
@[protected]
theorem linear_isometry.congr_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₂] {f g : E →ₛₗᵢ[σ₁₂] E₂} (h : f = g) (x : E) :
f x = g x
@[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_neg {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) :
f (-x) = -f x
@[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) :
@[protected]
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.is_complete_image_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₂) {s : set E} :
theorem linear_isometry.is_complete_map_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₂) [ring_hom_surjective σ₁₂] {p : submodule R E} :
@[protected, instance]
def linear_isometry.complete_space_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₂) [ring_hom_surjective σ₁₂] (p : submodule R E) [complete_space p] :
@[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) :
@[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) :
@[protected]
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
@[protected]
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₂) :
@[protected]
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₂) :
@[protected, continuity]
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
theorem linear_isometry.to_continuous_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₂] :
@[simp]
theorem linear_isometry.to_continuous_linear_map_inj {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₂} :
@[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) :
@[protected, 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)
@[protected, 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
theorem linear_isometry.one_def {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
theorem linear_isometry.mul_def {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.comp 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.

Instances for linear_isometry_equiv
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₂] :
@[simp]
theorem linear_isometry_equiv.to_linear_equiv_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
@[protected, instance]
def linear_isometry_equiv.add_monoid_hom_class {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₂] :
add_monoid_hom_class (E ≃ₛₗᵢ[σ₁₂] E₂) E E₂
Equations
@[protected, 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₂)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] :
@[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₂) :
@[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'
@[protected]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] {f : E ≃ₛₗᵢ[σ₁₂] E₂} {x x' : E} :
x = x'f x = f x'
@[protected]
theorem linear_isometry_equiv.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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} (h : f = g) (x : E) :
f x = g x
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
theorem linear_isometry_equiv.to_linear_isometry_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₂] :
@[simp]
theorem linear_isometry_equiv.to_linear_isometry_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
@[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₂) :
@[protected]
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
theorem linear_isometry_equiv.to_isometric_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₂] :
@[simp]
theorem linear_isometry_equiv.to_isometric_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
@[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
theorem linear_isometry_equiv.to_homeomorph_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₂] :
@[simp]
theorem linear_isometry_equiv.to_homeomorph_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
@[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₂) :
@[protected]
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₂) :
@[protected]
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} :
@[protected]
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} :
@[protected]
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
theorem linear_isometry_equiv.to_continuous_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₂] :
@[simp]
theorem linear_isometry_equiv.to_continuous_linear_equiv_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} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [semi_normed_group E] [semi_normed_group E₂] [module R E] [module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
@[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
@[protected, 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_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₂} [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₃) (c : E) :
(e₁.trans e₂) c = e₂ (e₁ c)
@[simp]
theorem linear_isometry_equiv.to_linear_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₃) :
@[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.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} [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_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} [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_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} [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.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} [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} {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.trans e₁.symm
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₄
@[protected, 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) :
theorem linear_isometry_equiv.one_def {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] :
theorem linear_isometry_equiv.mul_def {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'.trans e
theorem linear_isometry_equiv.inv_def {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] (e : E ≃ₗᵢ[R] E) :

Lemmas about mixing the group structure with definitions. Because we have multiple ways to express linear_isometry_equiv.refl, linear_isometry_equiv.symm, and linear_isometry_equiv.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 linear_isometry_equiv.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} [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.trans 1 = e
@[simp]
theorem linear_isometry_equiv.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} [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₂) :
1.trans e = e
@[simp]
theorem linear_isometry_equiv.refl_mul {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] (e : E ≃ₗᵢ[R] E) :
@[simp]
theorem linear_isometry_equiv.mul_refl {R : Type u_1} {E : Type u_5} [semiring R] [semi_normed_group E] [module R E] (e : E ≃ₗᵢ[R] E) :
@[protected, 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
@[protected, 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) :
@[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) :
@[protected]
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₂) :
@[protected]
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₂) :
@[protected]
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
@[protected]
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₂) :
@[protected]
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} :
@[protected, instance]
def linear_isometry_equiv.complete_space_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₂) (p : submodule R E) [complete_space p] :
noncomputable 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
@[simp]
theorem linear_isometry_equiv.coe_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) :
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] :
def linear_isometry_equiv.prod_assoc (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [semiring R] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group 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
@[simp]
theorem linear_isometry_equiv.coe_prod_assoc (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [semiring R] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [module R E] [module R E₂] [module R E₃] :
@[simp]
theorem linear_isometry_equiv.coe_prod_assoc_symm (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [semiring R] [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [module R E] [module R E₂] [module R E₃] :
theorem basis.ext_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₂] {ι : Type u_3} (b : basis ι R E) {f₁ 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_linear_isometry_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₂] {ι : Type u_3} (b : basis ι R E) {f₁ 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.