(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.
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₂} :
f.to_linear_map = g.to_linear_map ↔ f = g
@[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
- linear_isometry.add_monoid_hom_class = {coe := λ (e : E →ₛₗᵢ[σ₁₂] E₂), e.to_linear_map.to_fun, coe_injective' := _, map_add := _, map_zero := _}
@[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 to_fun.to_coe_fn directly.
Equations
- linear_isometry.has_coe_to_fun = {coe := λ (f : E →ₛₗᵢ[σ₁₂] E₂), f.to_linear_map.to_fun}
@[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₂) :
⇑(f.to_linear_map) = ⇑f
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} :
@[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) :
@[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₂) :
@[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) :
@[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} :
is_complete (⇑f '' s) ↔ is_complete s
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] :
@[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₂) :
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) :
@[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₂) :
lipschitz_with 1 ⇑f
@[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) :
emetric.diam (⇑f '' s) = emetric.diam s
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) :
metric.diam (⇑f '' s) = metric.diam s
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₂) :
Interpret a linear isometry as a continuous linear map.
Equations
- f.to_continuous_linear_map = {to_linear_map := f.to_linear_map, cont := _}
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₂) :
⇑(f.to_continuous_linear_map) = ⇑f
@[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} :
continuous (⇑f ∘ g) ↔ continuous g
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
- linear_isometry.id = {to_linear_map := linear_map.id _inst_29, norm_map' := _}
@[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) :
⇑linear_isometry.id x = x
@[simp]
theorem
linear_isometry.id_to_linear_map
{R : Type u_1}
{E : Type u_5}
[semiring R]
[semi_normed_group E]
[module R 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
- linear_isometry.inhabited = {default := linear_isometry.id _inst_29}
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₂) :
Composition of linear isometries.
Equations
- g.comp f = {to_linear_map := g.to_linear_map.comp f.to_linear_map, norm_map' := _}
@[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₂) :
@[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₂) :
linear_isometry.id.comp f = f
@[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₂) :
f.comp linear_isometry.id = f
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₂) :
@[protected, instance]
def
linear_isometry.monoid
{R : Type u_1}
{E : Type u_5}
[semiring R]
[semi_normed_group E]
[module R E] :
Equations
- linear_isometry.monoid = {mul := linear_isometry.comp _inst_29, mul_assoc := _, one := linear_isometry.id _inst_29, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (E →ₗᵢ[R] E)), npow_zero' := _, npow_succ' := _}
@[simp]
theorem
linear_isometry.coe_one
{R : Type u_1}
{E : Type u_5}
[semiring R]
[semi_normed_group E]
[module R E] :
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) :
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) :
Construct a linear_isometry from a linear_map satisfying isometry.
Equations
- f.to_linear_isometry hf = {to_linear_map := {to_fun := f.to_fun, map_add' := _, map_smul' := _}, norm_map' := _}
def
submodule.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) :
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.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.
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₂} :
f.to_linear_equiv = g.to_linear_equiv ↔ f = g
@[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
- linear_isometry_equiv.add_monoid_hom_class = {coe := λ (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.to_linear_equiv.to_fun, coe_injective' := _, map_add := _, map_zero := _}
@[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 to_fun.to_coe_fn directly.
Equations
- linear_isometry_equiv.has_coe_to_fun = {coe := λ (f : E ≃ₛₗᵢ[σ₁₂] E₂), f.to_linear_equiv.to_fun}
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₂) :
⇑(e.to_linear_equiv) = ⇑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} :
@[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) :
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∥) :
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' := _}
@[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₂) :
Reinterpret a linear_isometry_equiv as a linear_isometry.
Equations
- e.to_linear_isometry = {to_linear_map := ↑(e.to_linear_equiv), norm_map' := _}
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₂} :
f.to_linear_isometry = g.to_linear_isometry ↔ f = g
@[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₂) :
⇑(e.to_linear_isometry) = ⇑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
- e.to_isometric = {to_equiv := e.to_linear_equiv.to_equiv, isometry_to_fun := _}
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₂} :
f.to_isometric = g.to_isometric ↔ f = g
@[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₂) :
⇑(e.to_isometric) = ⇑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₂} :
f.to_homeomorph = g.to_homeomorph ↔ f = g
@[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₂) :
⇑(e.to_homeomorph) = ⇑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} :
continuous_at ⇑e x
@[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} :
continuous_on ⇑e s
@[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} :
continuous_within_at ⇑e s x
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₂) :
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 := _}
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
- linear_isometry_equiv.refl R E = {to_linear_equiv := linear_equiv.refl R E _inst_29, norm_map' := _}
@[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
- linear_isometry_equiv.inhabited = {default := linear_isometry_equiv.refl R E _inst_29}
@[simp]
theorem
linear_isometry_equiv.coe_refl
{R : Type u_1}
{E : Type u_5}
[semiring R]
[semi_normed_group E]
[module R E] :
⇑(linear_isometry_equiv.refl R E) = id
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₂) :
The inverse linear_isometry_equiv.
Equations
- e.symm = {to_linear_equiv := e.to_linear_equiv.symm, norm_map' := _}
@[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₂) :
@[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) :
@[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} :
@[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₂) :
@[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₃) :
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' := _}
@[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₃) :
@[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₃) :
(e.trans e').to_linear_equiv = e.to_linear_equiv.trans e'.to_linear_equiv
@[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₂) :
e.trans (linear_isometry_equiv.refl R₂ 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₂) :
(linear_isometry_equiv.refl R E).trans 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₂) :
e.trans e.symm = linear_isometry_equiv.refl R 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₂) :
e.symm.trans e = linear_isometry_equiv.refl R₂ 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₃) :
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₃) :
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₄) :
@[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
- linear_isometry_equiv.group = {mul := λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁, mul_assoc := _, one := linear_isometry_equiv.refl R E _inst_29, 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.group._proof_6 linear_isometry_equiv.group._proof_7, npow_zero' := _, npow_succ' := _, inv := linear_isometry_equiv.symm _inst_29, div := div_inv_monoid.div._default (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_10 (linear_isometry_equiv.refl R E) linear_isometry_equiv.group._proof_11 linear_isometry_equiv.group._proof_12 (div_inv_monoid.npow._default (linear_isometry_equiv.refl R E) (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_6 linear_isometry_equiv.group._proof_7) linear_isometry_equiv.group._proof_13 linear_isometry_equiv.group._proof_14 linear_isometry_equiv.symm, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_16 (linear_isometry_equiv.refl R E) linear_isometry_equiv.group._proof_17 linear_isometry_equiv.group._proof_18 (div_inv_monoid.npow._default (linear_isometry_equiv.refl R E) (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_6 linear_isometry_equiv.group._proof_7) linear_isometry_equiv.group._proof_19 linear_isometry_equiv.group._proof_20 linear_isometry_equiv.symm, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem
linear_isometry_equiv.coe_one
{R : Type u_1}
{E : Type u_5}
[semiring R]
[semi_normed_group E]
[module 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] :
1 = linear_isometry_equiv.refl 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) :
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) :
@[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₂] :
Reinterpret a linear_isometry_equiv as a continuous_linear_equiv.
Equations
- linear_isometry_equiv.continuous_linear_equiv.has_coe_t = {coe := λ (e : E ≃ₛₗᵢ[σ₁₂] E₂), {to_linear_equiv := e.to_linear_equiv, continuous_to_fun := _, continuous_inv_fun := _}}
@[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₂] :
@[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₂) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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} :
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) :
@[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₂) :
lipschitz_with 1 ⇑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) :
emetric.diam (⇑e '' s) = emetric.diam s
@[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) :
metric.diam (⇑e '' s) = metric.diam s
@[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 α} :
continuous_on (⇑e ∘ f) s ↔ continuous_on f s
@[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} :
continuous (⇑e ∘ f) ↔ continuous f
@[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) :
Construct a linear isometry equiv from a surjective linear isometry.
Equations
- linear_isometry_equiv.of_surjective f hfr = {to_linear_equiv := {to_fun := (linear_equiv.of_bijective f.to_linear_map _ hfr).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.of_bijective f.to_linear_map _ hfr).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
@[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) :
⇑(linear_isometry_equiv.of_surjective f hfr) = ⇑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
- linear_isometry_equiv.neg R = {to_linear_equiv := {to_fun := (linear_equiv.neg R).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.neg R).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
linear_isometry_equiv.coe_neg
{R : Type u_1}
{E : Type u_5}
[semiring R]
[semi_normed_group E]
[module R E] :
⇑(linear_isometry_equiv.neg R) = λ (x : E), -x
@[simp]
theorem
linear_isometry_equiv.symm_neg
{R : Type u_1}
{E : Type u_5}
[semiring R]
[semi_normed_group E]
[module R E] :
noncomputable
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₃] :
The natural equivalence (E × E₂) × E₃ ≃ E × (E₂ × E₃) is a linear isometry.
Equations
- linear_isometry_equiv.prod_assoc R E E₂ E₃ = {to_linear_equiv := {to_fun := ⇑(equiv.prod_assoc E E₂ E₃), map_add' := _, map_smul' := _, inv_fun := ⇑((equiv.prod_assoc E E₂ E₃).symm), left_inv := _, right_inv := _}, norm_map' := _}
@[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₃] :
⇑(linear_isometry_equiv.prod_assoc R E E₂ E₃) = ⇑(equiv.prod_assoc E E₂ 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₃] :
⇑((linear_isometry_equiv.prod_assoc R E E₂ E₃).symm) = ⇑((equiv.prod_assoc E E₂ E₃).symm)
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.