analysis.normed_space.linear_isometry

source

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)

to_linear_map : E →ₗ[R] F
norm_map' : ∀ (x : E), ∥⇑(c.to_linear_map) x∥ = ∥x∥

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

source

@[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] :

has_coe_to_fun (E →ₗᵢ[R] F)

Equations

linear_isometry.has_coe_to_fun = {F := λ (f : E →ₗᵢ[R] F), E → F, coe := λ (f : E →ₗᵢ[R] F), f.to_linear_map.to_fun}

source

@[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) :

⇑(f.to_linear_map) = ⇑f

source

theorem linear_isometry.to_linear_map_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 linear_isometry.to_linear_map

source

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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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) :

∥⇑f x∥ = ∥x∥

source

@[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) :

∥⇑f x∥₊ = ∥x∥₊

source

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) :

isometry ⇑f

source

@[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

source

@[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

source

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) :

function.injective ⇑f₁

source

@[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

source

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

source

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) :

lipschitz_with 1 ⇑f

source

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) :

antilipschitz_with 1 ⇑f

source

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) :

continuous ⇑f

source

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) :

emetric.diam (⇑f '' s) = emetric.diam s

source

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) :

emetric.diam (set.range ⇑f) = emetric.diam set.univ

source

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) :

metric.diam (⇑f '' s) = metric.diam s

source

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) :

metric.diam (set.range ⇑f) = metric.diam set.univ

source

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

f.to_continuous_linear_map = {to_linear_map := f.to_linear_map, cont := _}

source

@[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) :

⇑(f.to_continuous_linear_map) = ⇑f

source

@[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} :

continuous (⇑f ∘ g) ↔ continuous g

source

def linear_isometry.id {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

E →ₗᵢ[R] E

The identity linear isometry.

Equations

linear_isometry.id = {to_linear_map := linear_map.id _inst_6, norm_map' := _}

source

@[simp]

theorem linear_isometry.coe_id {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

⇑linear_isometry.id = ⇑linear_isometry.id

source

@[instance]

def linear_isometry.inhabited {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

inhabited (E →ₗᵢ[R] E)

Equations

linear_isometry.inhabited = {default := linear_isometry.id _inst_6}

source

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) :

E →ₗᵢ[R] G

Composition of linear isometries.

Equations

g.comp f = {to_linear_map := g.to_linear_map.comp f.to_linear_map, norm_map' := _}

source

@[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

source

@[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) :

linear_isometry.id.comp f = f

source

@[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) :

f.comp linear_isometry.id = f

source

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)

source

@[instance]

def linear_isometry.monoid {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

monoid (E →ₗᵢ[R] E)

Equations

linear_isometry.monoid = {mul := linear_isometry.comp _inst_6, mul_assoc := _, one := linear_isometry.id _inst_6, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (E →ₗᵢ[R] E)), npow_zero' := _, npow_succ' := _}

source

@[simp]

theorem linear_isometry.coe_one {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

⇑1 = ⇑linear_isometry.id

source

@[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

source

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

↥p →ₗᵢ[R'] E

submodule.subtype as a linear_isometry.

Equations

p.subtypeₗᵢ = {to_linear_map := p.subtype, norm_map' := _}

source

@[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) :

⇑(p.subtypeₗᵢ) = ⇑(p.subtype)

source

@[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) :

p.subtypeₗᵢ.to_linear_map = p.subtype

source

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

p.subtypeL = p.subtypeₗᵢ.to_continuous_linear_map

source

@[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) :

↑(p.subtypeL) = p.subtype

source

@[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) :

⇑(p.subtypeL) = ⇑(p.subtype)

source

@[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) :

p.subtypeL.range = p

source

@[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) :

p.subtypeL.ker = ⊥

source

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)

to_linear_equiv : E ≃ₗ[R] F
norm_map' : ∀ (x : E), ∥⇑(c.to_linear_equiv) x∥ = ∥x∥

A linear isometric equivalence between two normed vector spaces.

source

@[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] :

has_coe_to_fun (E ≃ₗᵢ[R] F)

Equations

linear_isometry_equiv.has_coe_to_fun = {F := λ (f : E ≃ₗᵢ[R] F), E → F, coe := λ (f : E ≃ₗᵢ[R] F), f.to_linear_equiv.to_fun}

source

@[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∥) :

⇑{to_linear_equiv := e, norm_map' := he} = ⇑e

source

@[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) :

⇑(e.to_linear_equiv) = ⇑e

source

theorem linear_isometry_equiv.to_linear_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] :

function.injective linear_isometry_equiv.to_linear_equiv

source

@[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'

source

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∥) :

E ≃ₗᵢ[R] F

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

Equations

linear_isometry_equiv.of_bounds e h₁ h₂ = {to_linear_equiv := e, norm_map' := _}

source

@[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) :

∥⇑e x∥ = ∥x∥

source

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) :

E →ₗᵢ[R] F

Reinterpret a linear_isometry_equiv as a linear_isometry.

Equations

e.to_linear_isometry = {to_linear_map := ↑(e.to_linear_equiv), norm_map' := _}

source

@[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) :

⇑(e.to_linear_isometry) = ⇑e

source

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) :

isometry ⇑e

source

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

e.to_isometric = {to_equiv := e.to_linear_equiv.to_equiv, isometry_to_fun := _}

source

@[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) :

⇑(e.to_isometric) = ⇑e

source

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) :

set.range ⇑e = set.univ

source

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

e.to_homeomorph = e.to_isometric.to_homeomorph

source

@[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) :

⇑(e.to_homeomorph) = ⇑e

source

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) :

continuous ⇑e

source

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} :

continuous_at ⇑e x

source

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} :

continuous_on ⇑e s

source

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} :

continuous_within_at ⇑e s x

source

def linear_isometry_equiv.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) :

E ≃L[R] F

Interpret a linear_isometry_equiv as a continuous linear equiv.

Equations

e.to_continuous_linear_equiv = {to_linear_equiv := {to_fun := e.to_linear_isometry.to_continuous_linear_map.to_linear_map.to_fun, map_add' := _, map_smul' := _, inv_fun := e.to_homeomorph.to_equiv.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

source

@[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) :

⇑(e.to_continuous_linear_equiv) = ⇑e

source

def linear_isometry_equiv.refl (R : Type u_1) (E : Type u_2) [semiring R] [semi_normed_group E] [module R E] :

E ≃ₗᵢ[R] E

Identity map as a linear_isometry_equiv.

Equations

linear_isometry_equiv.refl R E = {to_linear_equiv := linear_equiv.refl R E _inst_6, norm_map' := _}

source

@[instance]

def linear_isometry_equiv.inhabited {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

inhabited (E ≃ₗᵢ[R] E)

Equations

linear_isometry_equiv.inhabited = {default := linear_isometry_equiv.refl R E _inst_6}

source

@[simp]

theorem linear_isometry_equiv.coe_refl {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

⇑(linear_isometry_equiv.refl R E) = id

source

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) :

F ≃ₗᵢ[R] E

The inverse linear_isometry_equiv.

Equations

e.symm = {to_linear_equiv := e.to_linear_equiv.symm, norm_map' := _}

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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) :

e.to_linear_equiv.symm = e.symm.to_linear_equiv

source

@[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) :

e.to_isometric.symm = e.symm.to_isometric

source

@[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) :

e.to_homeomorph.symm = e.symm.to_homeomorph

source

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) :

E ≃ₗᵢ[R] G

Composition of linear_isometry_equivs as a linear_isometry_equiv.

Equations

e.trans e' = {to_linear_equiv := e.to_linear_equiv.trans e'.to_linear_equiv, norm_map' := _}

source

@[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₁

source

@[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) :

e.trans (linear_isometry_equiv.refl R F) = e

source

@[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) :

(linear_isometry_equiv.refl R E).trans e = e

source

@[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) :

e.trans e.symm = linear_isometry_equiv.refl R E

source

@[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) :

e.symm.trans e = linear_isometry_equiv.refl R F

source

@[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)

source

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'

source

@[instance]

def linear_isometry_equiv.group {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

group (E ≃ₗᵢ[R] E)

Equations

linear_isometry_equiv.group = {mul := λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁, mul_assoc := _, one := linear_isometry_equiv.refl R E _inst_6, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (linear_isometry_equiv.refl R E) (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.trans_refl linear_isometry_equiv.refl_trans, npow_zero' := _, npow_succ' := _, inv := linear_isometry_equiv.symm _inst_6, div := div_inv_monoid.div._default (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_4 (linear_isometry_equiv.refl R E) linear_isometry_equiv.trans_refl linear_isometry_equiv.refl_trans (div_inv_monoid.npow._default (linear_isometry_equiv.refl R E) (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.trans_refl linear_isometry_equiv.refl_trans) linear_isometry_equiv.group._proof_5 linear_isometry_equiv.group._proof_6 linear_isometry_equiv.symm, div_eq_mul_inv := _, gpow := div_inv_monoid.gpow._default (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_8 (linear_isometry_equiv.refl R E) linear_isometry_equiv.trans_refl linear_isometry_equiv.refl_trans (div_inv_monoid.npow._default (linear_isometry_equiv.refl R E) (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.trans_refl linear_isometry_equiv.refl_trans) linear_isometry_equiv.group._proof_9 linear_isometry_equiv.group._proof_10 linear_isometry_equiv.symm, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _}

source

@[simp]

theorem linear_isometry_equiv.coe_one {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

⇑1 = id

source

@[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'

source

@[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) :

⇑e⁻¹ = ⇑(e.symm)

source

@[instance]

def linear_isometry_equiv.continuous_linear_equiv.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] :

has_coe_t (E ≃ₗᵢ[R] F) (E ≃L[R] F)

Reinterpret a linear_isometry_equiv as a continuous_linear_equiv.

Equations

linear_isometry_equiv.continuous_linear_equiv.has_coe_t = {coe := λ (e : E ≃ₗᵢ[R] F), {to_linear_equiv := e.to_linear_equiv, continuous_to_fun := _, continuous_inv_fun := _}}

source

@[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] :

has_coe_t (E ≃ₗᵢ[R] F) (E →L[R] F)

Equations

linear_isometry_equiv.continuous_linear_map.has_coe_t = {coe := λ (e : E ≃ₗᵢ[R] F), ↑↑e}

source

@[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) :

⇑↑e = ⇑e

source

@[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) :

↑↑e = ↑e

source

@[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) :

⇑↑e = ⇑e

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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) :

∥⇑e x∥₊ = ∥x∥₊

source

@[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

source

@[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

source

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) :

function.bijective ⇑e

source

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) :

function.injective ⇑e

source

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) :

function.surjective ⇑e

source

@[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

source

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

source

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) :

lipschitz_with 1 ⇑e

source

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) :

antilipschitz_with 1 ⇑e

source

@[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) :

emetric.diam (⇑e '' s) = emetric.diam s

source

@[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) :

metric.diam (⇑e '' s) = metric.diam s

source

@[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 α} :

continuous_on (⇑e ∘ f) s ↔ continuous_on f s

source

@[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} :

continuous (⇑e ∘ f) ↔ continuous f

source

@[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) :

⇑linear_isometry.id x = x

source

@[simp]

theorem linear_isometry_equiv.linear_isometry.id_to_linear_map {R : Type u_1} {E : Type u_2} [semiring R] [semi_normed_group E] [module R E] :

linear_isometry.id.to_linear_map = linear_map.id

source

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

li.to_linear_isometry_equiv h = {to_linear_equiv := li.to_linear_map.linear_equiv_of_ker_eq_bot _ h, norm_map' := _}

source

@[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) :

⇑(li.to_linear_isometry_equiv h) = ⇑li

source

@[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₁) :

⇑(li.to_linear_isometry_equiv h) x = ⇑li x

mathlib documentation

Linear isometries #