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.
An R
-linear isometric embedding of one normed R
-module into another.
Interpret a linear isometry as a continuous linear map.
Equations
- f.to_continuous_linear_map = {to_linear_map := f.to_linear_map, cont := _}
The identity linear isometry.
Equations
- linear_isometry.id = {to_linear_map := linear_map.id _inst_6, norm_map' := _}
Equations
- linear_isometry.inhabited = {default := linear_isometry.id _inst_6}
Composition of linear isometries.
Equations
- g.comp f = {to_linear_map := g.to_linear_map.comp f.to_linear_map, norm_map' := _}
Equations
- linear_isometry.monoid = {mul := linear_isometry.comp _inst_6, mul_assoc := _, one := linear_isometry.id _inst_6, one_mul := _, mul_one := _}
submodule.subtype
as a continuous_linear_map
.
Equations
A linear isometric equivalence between two normed vector spaces.
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' := _}
Reinterpret a linear_isometry_equiv
as a linear_isometry
.
Equations
- e.to_linear_isometry = {to_linear_map := ↑(e.to_linear_equiv), norm_map' := _}
Reinterpret a linear_isometry_equiv
as an isometric
.
Equations
- e.to_isometric = {to_equiv := e.to_linear_equiv.to_equiv, isometry_to_fun := _}
Reinterpret a linear_isometry_equiv
as an homeomorph
.
Equations
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' := _}
Equations
- linear_isometry_equiv.inhabited = {default := linear_isometry_equiv.refl R E _inst_6}
The inverse linear_isometry_equiv
.
Equations
- e.symm = {to_linear_equiv := e.to_linear_equiv.symm, norm_map' := _}
Composition of linear_isometry_equiv
s as a linear_isometry_equiv
.
Equations
- e.trans e' = {to_linear_equiv := e.to_linear_equiv.trans e'.to_linear_equiv, norm_map' := _}
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 := _, 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_2 (linear_isometry_equiv.refl R E) linear_isometry_equiv.trans_refl linear_isometry_equiv.refl_trans linear_isometry_equiv.symm, div_eq_mul_inv := _, mul_left_inv := _}
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 := _}}