mathlib documentation

analysis.normed_space.linear_isometry

Linear isometries #

In this file we define linear_isometry R E F (notation: E →ₗᵢ[R] F) to be a linear isometric embedding of E into F and linear_isometry_equiv (notation: E ≃ₗᵢ[R] F) to be a linear isometric equivalence between E and F.

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_7) (E : Type u_8) (F : Type u_9) [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] :
Type (max u_8 u_9)

An R-linear isometric embedding of one normed R-module into another.

@[instance]
def linear_isometry.has_coe_to_fun {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] :
Equations
@[simp]
theorem linear_isometry.coe_to_linear_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
theorem linear_isometry.coe_fn_injective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] :
function.injective (λ (f : E →ₗᵢ[R] F) (x : E), f x)
@[ext]
theorem linear_isometry.ext {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] {f g : E →ₗᵢ[R] F} (h : ∀ (x : E), f x = g x) :
f = g
@[simp]
theorem linear_isometry.map_zero {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
f 0 = 0
@[simp]
theorem linear_isometry.map_add {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) (x y : E) :
f (x + y) = f x + f y
@[simp]
theorem linear_isometry.map_sub {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) (x y : E) :
f (x - y) = f x - f y
@[simp]
theorem linear_isometry.map_smul {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) (c : R) (x : E) :
f (c x) = c f x
@[simp]
theorem linear_isometry.norm_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) (x : E) :
@[simp]
theorem linear_isometry.nnnorm_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) (x : E) :
theorem linear_isometry.isometry {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
@[simp]
theorem linear_isometry.dist_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) (x y : E) :
dist (f x) (f y) = dist x y
@[simp]
theorem linear_isometry.edist_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) (x y : E) :
edist (f x) (f y) = edist x y
theorem linear_isometry.injective {R : Type u_1} {F : Type u_3} {E₁ : Type u_6} [semiring R] [semi_normed_group F] [module R F] [normed_group E₁] [module R E₁] (f₁ : E₁ →ₗᵢ[R] F) :
@[simp]
theorem linear_isometry.map_eq_iff {R : Type u_1} {F : Type u_3} {E₁ : Type u_6} [semiring R] [semi_normed_group F] [module R F] [normed_group E₁] [module R E₁] (f₁ : E₁ →ₗᵢ[R] F) {x y : E₁} :
f₁ x = f₁ y x = y
theorem linear_isometry.map_ne {R : Type u_1} {F : Type u_3} {E₁ : Type u_6} [semiring R] [semi_normed_group F] [module R F] [normed_group E₁] [module R E₁] (f₁ : E₁ →ₗᵢ[R] F) {x y : E₁} (h : x y) :
f₁ x f₁ y
theorem linear_isometry.lipschitz {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
theorem linear_isometry.antilipschitz {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
theorem linear_isometry.continuous {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
theorem linear_isometry.ediam_image {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) (s : set E) :
theorem linear_isometry.ediam_range {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
theorem linear_isometry.diam_image {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) (s : set E) :
theorem linear_isometry.diam_range {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
def linear_isometry.to_continuous_linear_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
E →L[R] F

Interpret a linear isometry as a continuous linear map.

Equations
@[simp]
theorem linear_isometry.coe_to_continuous_linear_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
@[simp]
theorem linear_isometry.comp_continuous_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) {α : Type u_4} [topological_space α] {g : α → E} :
def linear_isometry.id {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

The identity linear isometry.

Equations
@[simp]
@[instance]
def linear_isometry.inhabited {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :
Equations
def linear_isometry.comp {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semiring R] [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [module R E] [module R F] [module R G] (g : F →ₗᵢ[R] G) (f : E →ₗᵢ[R] F) :

Composition of linear isometries.

Equations
@[simp]
theorem linear_isometry.coe_comp {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semiring R] [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [module R E] [module R F] [module R G] (g : F →ₗᵢ[R] G) (f : E →ₗᵢ[R] F) :
(g.comp f) = g f
@[simp]
theorem linear_isometry.id_comp {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
@[simp]
theorem linear_isometry.comp_id {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (f : E →ₗᵢ[R] F) :
theorem linear_isometry.comp_assoc {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {G' : Type u_5} [semiring R] [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [semi_normed_group G'] [module R E] [module R F] [module R G] [module R G'] (f : G →ₗᵢ[R] G') (g : F →ₗᵢ[R] G) (h : E →ₗᵢ[R] F) :
(f.comp g).comp h = f.comp (g.comp h)
@[instance]
def linear_isometry.monoid {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :
Equations
@[simp]
theorem linear_isometry.coe_one {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :
@[simp]
theorem linear_isometry.coe_mul {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] (f g : E →ₗᵢ[R] E) :
f * g = f g
def submodule.subtypeₗᵢ {E : Type u_2} [semi_normed_group E] {R' : Type u_7} [ring R'] [module R' E] (p : submodule R' E) :

submodule.subtype as a linear_isometry.

Equations
@[simp]
theorem submodule.coe_subtypeₗᵢ {E : Type u_2} [semi_normed_group E] {R' : Type u_7} [ring R'] [module R' E] (p : submodule R' E) :
@[simp]
theorem submodule.subtypeₗᵢ_to_linear_map {E : Type u_2} [semi_normed_group E] {R' : Type u_7} [ring R'] [module R' E] (p : submodule R' E) :
def submodule.subtypeL {E : Type u_2} [semi_normed_group E] {R' : Type u_7} [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_2} [semi_normed_group E] {R' : Type u_7} [ring R'] [module R' E] (p : submodule R' E) :
@[simp]
theorem submodule.coe_subtypeL' {E : Type u_2} [semi_normed_group E] {R' : Type u_7} [ring R'] [module R' E] (p : submodule R' E) :
@[simp]
theorem submodule.range_subtypeL {E : Type u_2} [semi_normed_group E] {R' : Type u_7} [ring R'] [module R' E] (p : submodule R' E) :
@[simp]
theorem submodule.ker_subtypeL {E : Type u_2} [semi_normed_group E] {R' : Type u_7} [ring R'] [module R' E] (p : submodule R' E) :
structure linear_isometry_equiv (R : Type u_7) (E : Type u_8) (F : Type u_9) [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] :
Type (max u_8 u_9)

A linear isometric equivalence between two normed vector spaces.

@[instance]
def linear_isometry_equiv.has_coe_to_fun {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] :
Equations
@[simp]
theorem linear_isometry_equiv.coe_mk {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗ[R] F) (he : ∀ (x : E), e x = x) :
@[simp]
theorem linear_isometry_equiv.coe_to_linear_equiv {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[ext]
theorem linear_isometry_equiv.ext {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] {e e' : E ≃ₗᵢ[R] F} (h : ∀ (x : E), e x = e' x) :
e = e'
def linear_isometry_equiv.of_bounds {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗ[R] F) (h₁ : ∀ (x : E), e x x) (h₂ : ∀ (y : F), (e.symm) y y) :

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} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (x : E) :
def linear_isometry_equiv.to_linear_isometry {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :

Reinterpret a linear_isometry_equiv as a linear_isometry.

Equations
@[simp]
theorem linear_isometry_equiv.coe_to_linear_isometry {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
theorem linear_isometry_equiv.isometry {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
def linear_isometry_equiv.to_isometric {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
E ≃ᵢ F

Reinterpret a linear_isometry_equiv as an isometric.

Equations
@[simp]
theorem linear_isometry_equiv.coe_to_isometric {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
theorem linear_isometry_equiv.range_eq_univ {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
def linear_isometry_equiv.to_homeomorph {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
E ≃ₜ F

Reinterpret a linear_isometry_equiv as an homeomorph.

Equations
@[simp]
theorem linear_isometry_equiv.coe_to_homeomorph {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
theorem linear_isometry_equiv.continuous {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
theorem linear_isometry_equiv.continuous_at {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) {x : E} :
theorem linear_isometry_equiv.continuous_on {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) {s : set E} :
theorem linear_isometry_equiv.continuous_within_at {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) {s : set E} {x : E} :
@[simp]
theorem linear_isometry_equiv.coe_to_continuous_linear_equiv {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
def linear_isometry_equiv.refl (R : Type u_1) (E : Type u_2) [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_2} [semiring R] [semi_normed_group E] [module R E] :
Equations
@[simp]
theorem linear_isometry_equiv.coe_refl {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :
def linear_isometry_equiv.symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :

The inverse linear_isometry_equiv.

Equations
@[simp]
theorem linear_isometry_equiv.apply_symm_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (x : F) :
e ((e.symm) x) = x
@[simp]
theorem linear_isometry_equiv.symm_apply_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (x : E) :
(e.symm) (e x) = x
@[simp]
theorem linear_isometry_equiv.map_eq_zero_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) {x : E} :
e x = 0 x = 0
@[simp]
theorem linear_isometry_equiv.symm_symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
e.symm.symm = e
@[simp]
theorem linear_isometry_equiv.to_linear_equiv_symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.to_isometric_symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.to_homeomorph_symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
def linear_isometry_equiv.trans {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semiring R] [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [module R E] [module R F] [module R G] (e : E ≃ₗᵢ[R] F) (e' : F ≃ₗᵢ[R] G) :

Composition of linear_isometry_equivs as a linear_isometry_equiv.

Equations
@[simp]
theorem linear_isometry_equiv.coe_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semiring R] [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [module R E] [module R F] [module R G] (e₁ : E ≃ₗᵢ[R] F) (e₂ : F ≃ₗᵢ[R] G) :
(e₁.trans e₂) = e₂ e₁
@[simp]
theorem linear_isometry_equiv.trans_refl {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.refl_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.trans_symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.symm_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.coe_symm_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semiring R] [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [module R E] [module R F] [module R G] (e₁ : E ≃ₗᵢ[R] F) (e₂ : F ≃ₗᵢ[R] G) :
((e₁.trans e₂).symm) = (e₁.symm) (e₂.symm)
theorem linear_isometry_equiv.trans_assoc {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {G' : Type u_5} [semiring R] [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [semi_normed_group G'] [module R E] [module R F] [module R G] [module R G'] (eEF : E ≃ₗᵢ[R] F) (eFG : F ≃ₗᵢ[R] G) (eGG' : G ≃ₗᵢ[R] G') :
eEF.trans (eFG.trans eGG') = (eEF.trans eFG).trans eGG'
@[instance]
def linear_isometry_equiv.group {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :
Equations
@[simp]
theorem linear_isometry_equiv.coe_one {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :
@[simp]
theorem linear_isometry_equiv.coe_mul {R : Type u_1} {E : Type u_2} [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_2} [semiring R] [semi_normed_group E] [module R E] (e : E ≃ₗᵢ[R] E) :
@[instance]
def linear_isometry_equiv.continuous_linear_map.has_coe_t {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] :
Equations
@[simp]
theorem linear_isometry_equiv.coe_coe {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.coe_coe' {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.coe_coe'' {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.map_zero {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
e 0 = 0
@[simp]
theorem linear_isometry_equiv.map_add {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (x y : E) :
e (x + y) = e x + e y
@[simp]
theorem linear_isometry_equiv.map_sub {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (x y : E) :
e (x - y) = e x - e y
@[simp]
theorem linear_isometry_equiv.map_smul {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (c : R) (x : E) :
e (c x) = c e x
@[simp]
theorem linear_isometry_equiv.nnnorm_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (x : E) :
@[simp]
theorem linear_isometry_equiv.dist_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (x y : E) :
dist (e x) (e y) = dist x y
@[simp]
theorem linear_isometry_equiv.edist_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (x y : E) :
edist (e x) (e y) = edist x y
theorem linear_isometry_equiv.bijective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
theorem linear_isometry_equiv.injective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
theorem linear_isometry_equiv.surjective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.map_eq_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) {x y : E} :
e x = e y x = y
theorem linear_isometry_equiv.map_ne {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) {x y : E} (h : x y) :
e x e y
theorem linear_isometry_equiv.lipschitz {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
theorem linear_isometry_equiv.antilipschitz {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) :
@[simp]
theorem linear_isometry_equiv.ediam_image {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (s : set E) :
@[simp]
theorem linear_isometry_equiv.diam_image {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) (s : set E) :
@[simp]
theorem linear_isometry_equiv.comp_continuous_on_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) {α : Type u_7} [topological_space α] {f : α → E} {s : set α} :
@[simp]
theorem linear_isometry_equiv.comp_continuous_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [semi_normed_group E] [semi_normed_group F] [module R E] [module R F] (e : E ≃ₗᵢ[R] F) {α : Type u_7} [topological_space α] {f : α → E} :
@[simp]
theorem linear_isometry_equiv.linear_isometry.id_apply {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] (x : E) :
def linear_isometry.to_linear_isometry_equiv {F : Type u_3} {E₁ : Type u_6} [semi_normed_group F] [normed_group E₁] {R₁ : Type u_7} [field R₁] [module R₁ E₁] [module R₁ F] [finite_dimensional R₁ E₁] [finite_dimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : finite_dimensional.finrank R₁ E₁ = finite_dimensional.finrank R₁ F) :
E₁ ≃ₗᵢ[R₁] F

A linear isometry between finite dimensional spaces of equal dimension can be upgraded to a linear isometry equivalence.

Equations
@[simp]
theorem linear_isometry.coe_to_linear_isometry_equiv {F : Type u_3} {E₁ : Type u_6} [semi_normed_group F] [normed_group E₁] {R₁ : Type u_7} [field R₁] [module R₁ E₁] [module R₁ F] [finite_dimensional R₁ E₁] [finite_dimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : finite_dimensional.finrank R₁ E₁ = finite_dimensional.finrank R₁ F) :
@[simp]
theorem linear_isometry.to_linear_isometry_equiv_apply {F : Type u_3} {E₁ : Type u_6} [semi_normed_group F] [normed_group E₁] {R₁ : Type u_7} [field R₁] [module R₁ E₁] [module R₁ F] [finite_dimensional R₁ E₁] [finite_dimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : finite_dimensional.finrank R₁ E₁ = finite_dimensional.finrank R₁ F) (x : E₁) :