# (Semi-)linear isometries #

In this file we define `LinearIsometry σ₁₂ E E₂` (notation: `E →ₛₗᵢ[σ₁₂] E₂`) to be a semilinear isometric embedding of `E` into `E₂` and `LinearIsometryEquiv` (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 `SeminormedAddCommGroup` and we specialize to `NormedAddCommGroup` when needed.

source
structure LinearIsometry {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] extends E →ₛₗ[σ₁₂] E₂ :
Type (max u_11 u_12)

A `σ₁₂`-semilinear isometric embedding of a normed `R`-module into an `R₂`-module, denoted as `f : E →ₛₗᵢ[σ₁₂] E₂`.

- toFun : E → E₂
- map_add' (x y : E) : self.toFun (x + y) = self.toFun x + self.toFun y
- map_smul' (m : R) (x : E) : self.toFun (m • x) = σ₁₂ m • self.toFun x
- norm_map' (x : E) : ‖self.toLinearMap x‖ = ‖x‖

Instances For

source
def «term_→ₛₗᵢ[_]_» :
Lean.TrailingParserDescr

A `σ₁₂`-semilinear isometric embedding of a normed `R`-module into an `R₂`-module, denoted as `f : E →ₛₗᵢ[σ₁₂] E₂`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def «term_→ₗᵢ[_]_» :
Lean.TrailingParserDescr

A linear isometric embedding of a normed `R`-module into another one.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def «term_→ₗᵢ⋆[_]_» :
Lean.TrailingParserDescr

An antilinear isometric embedding of a normed `R`-module into another one.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
class SemilinearIsometryClass (𝓕 : Type u_11) {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} [Semiring R] [Semiring R₂] (σ₁₂ : outParam (R →+* R₂)) (E : outParam (Type u_14)) (E₂ : outParam (Type u_15)) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] extends SemilinearMapClass 𝓕 σ₁₂ E E₂ :
Prop

`SemilinearIsometryClass F σ E E₂` asserts `F` is a type of bundled `σ`-semilinear isometries `E → E₂`.

See also `LinearIsometryClass F R E E₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S` is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and `f (c • x) = (σ c) • f x`.

- map_add (f : 𝓕) (x y : E) : f (x + y) = f x + f y
- map_smulₛₗ (f : 𝓕) (c : R) (x : E) : f (c • x) = σ₁₂ c • f x
- norm_map (f : 𝓕) (x : E) : ‖f x‖ = ‖x‖

Instances

source
@[reducible, inline]
abbrev LinearIsometryClass (𝓕 : Type u_11) (R : outParam (Type u_12)) (E : outParam (Type u_13)) (E₂ : outParam (Type u_14)) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] [FunLike 𝓕 E E₂] :
Prop

`LinearIsometryClass F R E E₂` asserts `F` is a type of bundled `R`-linear isometries `M → M₂`.

This is an abbreviation for `SemilinearIsometryClass F (RingHom.id R) E E₂`.

Equations

- LinearIsometryClass 𝓕 R E E₂ = SemilinearIsometryClass 𝓕 (RingHom.id R) E E₂

Instances For

source
theorem SemilinearIsometryClass.isometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
Isometry ⇑f
source
theorem SemilinearIsometryClass.continuous {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
Continuous ⇑f
source
theorem SemilinearIsometryClass.nnnorm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (x : E) :
‖f x‖₊ = ‖x‖₊
source
theorem SemilinearIsometryClass.lipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
LipschitzWith 1 ⇑f
source
theorem SemilinearIsometryClass.antilipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
AntilipschitzWith 1 ⇑f
source
theorem SemilinearIsometryClass.ediam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (s : Set E) :
EMetric.diam (⇑f '' s) = EMetric.diam s
source
theorem SemilinearIsometryClass.ediam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
EMetric.diam (Set.range ⇑f) = EMetric.diam Set.univ
source
theorem SemilinearIsometryClass.diam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (s : Set E) :
Metric.diam (⇑f '' s) = Metric.diam s
source
theorem SemilinearIsometryClass.diam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
source
@[instance 100]
instance SemilinearIsometryClass.toContinuousSemilinearMapClass {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] :
ContinuousSemilinearMapClass 𝓕 σ₁₂ E E₂
source
theorem LinearIsometry.toLinearMap_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Injective toLinearMap
source
@[simp]
theorem LinearIsometry.toLinearMap_inj {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂} :
f.toLinearMap = g.toLinearMap ↔ f = g
source
instance LinearIsometry.instFunLike {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
FunLike (E →ₛₗᵢ[σ₁₂] E₂) E E₂
Equations

- LinearIsometry.instFunLike = { coe := fun (f : E →ₛₗᵢ[σ₁₂] E₂) => f.toFun, coe_injective' := ⋯ }

source
instance LinearIsometry.instSemilinearIsometryClass {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
SemilinearIsometryClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
source
@[simp]
theorem LinearIsometry.coe_toLinearMap {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
⇑f.toLinearMap = ⇑f
source
@[simp]
theorem LinearIsometry.coe_mk {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) (hf : ∀ (x : E), ‖f x‖ = ‖x‖) :
⇑{ toLinearMap := f, norm_map' := hf } = ⇑f
source
theorem LinearIsometry.coe_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Injective fun (f : E →ₛₗᵢ[σ₁₂] E₂) => ⇑f
source
def LinearIsometry.Simps.apply {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E →ₛₗᵢ[σ₁₂] E₂) :
E → E₂

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

- LinearIsometry.Simps.apply σ₁₂ E E₂ h = ⇑h

Instances For

source
theorem LinearIsometry.ext {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ (x : E), f x = g x) :
f = g
source
theorem LinearIsometry.ext_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂} :
f = g ↔ ∀ (x : E), f x = g x
source
theorem LinearIsometry.map_zero {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
f 0 = 0
source
theorem LinearIsometry.map_add {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E) :
f (x + y) = f x + f y
source
theorem LinearIsometry.map_neg {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) :
f (-x) = -f x
source
theorem LinearIsometry.map_sub {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E) :
f (x - y) = f x - f y
source
theorem LinearIsometry.map_smulₛₗ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (c : R) (x : E) :
f (c • x) = σ₁₂ c • f x
source
theorem LinearIsometry.map_smul {R : Type u_1} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] (f : E →ₗᵢ[R] E₂) (c : R) (x : E) :
f (c • x) = c • f x
source
@[simp]
theorem LinearIsometry.norm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) :
‖f x‖ = ‖x‖
source
@[simp]
theorem LinearIsometry.nnnorm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) :
‖f x‖₊ = ‖x‖₊
source
@[simp]
theorem LinearIsometry.enorm_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) :
‖f x‖ₑ = ‖x‖ₑ
source
theorem LinearIsometry.isometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
Isometry ⇑f
source
theorem LinearIsometry.isEmbedding {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f : F →ₛₗᵢ[σ₁₂] E₂) :
Topology.IsEmbedding ⇑f
source
theorem LinearIsometry.isComplete_image_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) {s : Set E} :
IsComplete (⇑f '' s) ↔ IsComplete s
source
@[simp]
theorem LinearIsometry.isComplete_image_iff' {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) {s : Set E} :
IsComplete (⇑f '' s) ↔ IsComplete s
source
theorem LinearIsometry.isComplete_map_iff {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) [RingHomSurjective σ₁₂] {p : Submodule R E} :
IsComplete ↑(Submodule.map f.toLinearMap p) ↔ IsComplete ↑p
source
theorem LinearIsometry.isComplete_map_iff' {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) [RingHomSurjective σ₁₂] {p : Submodule R E} :
IsComplete ↑(Submodule.map f p) ↔ IsComplete ↑p
source
instance LinearIsometry.completeSpace_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) [RingHomSurjective σ₁₂] (p : Submodule R E) [CompleteSpace ↥p] :
CompleteSpace ↥(Submodule.map f p)
source
instance LinearIsometry.completeSpace_map' {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) [RingHomSurjective σ₁₂] (p : Submodule R E) [CompleteSpace ↥p] :
CompleteSpace ↥(Submodule.map f.toLinearMap p)
source
@[simp]
theorem LinearIsometry.dist_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E) :
dist (f x) (f y) = dist x y
source
@[simp]
theorem LinearIsometry.edist_map {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E) :
edist (f x) (f y) = edist x y
source
theorem LinearIsometry.injective {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) :
Function.Injective ⇑f₁
source
@[simp]
theorem LinearIsometry.map_eq_iff {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) {x y : F} :
f₁ x = f₁ y ↔ x = y
source
theorem LinearIsometry.map_ne {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) {x y : F} (h : x ≠ y) :
f₁ x ≠ f₁ y
source
theorem LinearIsometry.lipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
LipschitzWith 1 ⇑f
source
theorem LinearIsometry.antilipschitz {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
AntilipschitzWith 1 ⇑f
source
theorem LinearIsometry.continuous {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
Continuous ⇑f
source
@[simp]
theorem LinearIsometry.preimage_ball {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ) :
⇑f ⁻¹' Metric.ball (f x) r = Metric.ball x r
source
@[simp]
theorem LinearIsometry.preimage_sphere {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ) :
⇑f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
source
@[simp]
theorem LinearIsometry.preimage_closedBall {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ) :
⇑f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
source
theorem LinearIsometry.ediam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
EMetric.diam (⇑f '' s) = EMetric.diam s
source
theorem LinearIsometry.ediam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
EMetric.diam (Set.range ⇑f) = EMetric.diam Set.univ
source
theorem LinearIsometry.diam_image {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
Metric.diam (⇑f '' s) = Metric.diam s
source
theorem LinearIsometry.diam_range {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
source
def LinearIsometry.toContinuousLinearMap {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
E →SL[σ₁₂] E₂

Interpret a linear isometry as a continuous linear map.

Equations

- f.toContinuousLinearMap = { toLinearMap := f.toLinearMap, cont := ⋯ }

Instances For

source
theorem LinearIsometry.toContinuousLinearMap_injective {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Injective toContinuousLinearMap
source
@[simp]
theorem LinearIsometry.toContinuousLinearMap_inj {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂} :
f.toContinuousLinearMap = g.toContinuousLinearMap ↔ f = g
source
@[simp]
theorem LinearIsometry.coe_toContinuousLinearMap {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
⇑f.toContinuousLinearMap = ⇑f
source
@[simp]
theorem LinearIsometry.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₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) {α : Type u_11} [TopologicalSpace α] {g : α → E} :
Continuous (⇑f ∘ g) ↔ Continuous g
source
def LinearIsometry.id {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
E →ₗᵢ[R] E

The identity linear isometry.

Equations

- LinearIsometry.id = { toLinearMap := LinearMap.id, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometry.coe_id {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
⇑id = _root_.id
source
@[simp]
theorem LinearIsometry.id_apply {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (x : E) :
id x = x
source
@[simp]
theorem LinearIsometry.id_toLinearMap {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
id.toLinearMap = LinearMap.id
source
@[simp]
theorem LinearIsometry.id_toContinuousLinearMap {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
id.toContinuousLinearMap = ContinuousLinearMap.id R E
source
instance LinearIsometry.instInhabited {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
Inhabited (E →ₗᵢ[R] E)
Equations

- LinearIsometry.instInhabited = { default := LinearIsometry.id }

source
def LinearIsometry.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₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) :
E →ₛₗᵢ[σ₁₃] E₃

Composition of linear isometries.

Equations

- g.comp f = { toLinearMap := g.toLinearMap ∘ₛₗ f.toLinearMap, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometry.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₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) :
⇑(g.comp f) = ⇑g ∘ ⇑f
source
@[simp]
theorem LinearIsometry.id_comp {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
id.comp f = f
source
@[simp]
theorem LinearIsometry.comp_id {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) :
f.comp id = f
source
theorem LinearIsometry.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₄} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [SeminormedAddCommGroup E₄] [Module R E] [Module R₂ E₂] [Module R₃ E₃] [Module R₄ E₄] (f : E₃ →ₛₗᵢ[σ₃₄] E₄) (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (h : E →ₛₗᵢ[σ₁₂] E₂) :
(f.comp g).comp h = f.comp (g.comp h)
source
instance LinearIsometry.instMonoid {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
Monoid (E →ₗᵢ[R] E)
Equations

- LinearIsometry.instMonoid = { mul := LinearIsometry.comp, mul_assoc := ⋯, one := LinearIsometry.id, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

source
@[simp]
theorem LinearIsometry.coe_one {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
⇑1 = _root_.id
source
@[simp]
theorem LinearIsometry.coe_mul {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (f g : E →ₗᵢ[R] E) :
⇑(f * g) = ⇑f ∘ ⇑g
source
theorem LinearIsometry.one_def {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
1 = id
source
theorem LinearIsometry.mul_def {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (f g : E →ₗᵢ[R] E) :
f * g = f.comp g
source
theorem LinearIsometry.coe_pow {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (f : E →ₗᵢ[R] E) (n : ℕ) :
⇑(f ^ n) = (⇑f)^[n]
source
def LinearIsometry.submoduleMap {R : Type u_11} {M : Type u_14} {M₁ : Type u_15} [Ring R] [SeminormedAddCommGroup M] [SeminormedAddCommGroup M₁] [Module R M] [Module R M₁] (p : Submodule R M) (e : M →ₗᵢ[R] M₁) :
↥p →ₗᵢ[R] ↥(Submodule.map e p)

A linear isometry between two modules restricts to a linear isometry from any submodule `p` of the domain onto the image of that submodule.

This is a version of `LinearMap.submoduleMap` extended to linear isometries.

Equations

- LinearIsometry.submoduleMap p e = { toLinearMap := e.submoduleMap p, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometry.submoduleMap_apply_coe {R : Type u_11} {M : Type u_14} {M₁ : Type u_15} [Ring R] [SeminormedAddCommGroup M] [SeminormedAddCommGroup M₁] [Module R M] [Module R M₁] (p : Submodule R M) (e : M →ₗᵢ[R] M₁) (c : ↥p) :
↑((submoduleMap p e) c) = e ↑c
source
def LinearMap.toLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) (hf : Isometry ⇑f) :
E →ₛₗᵢ[σ₁₂] E₂

Construct a `LinearIsometry` from a `LinearMap` satisfying `Isometry`.

Equations

- f.toLinearIsometry hf = { toLinearMap := f, norm_map' := ⋯ }

Instances For

source
def Submodule.subtypeₗᵢ {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_11} [Ring R'] [Module R' E] (p : Submodule R' E) :
↥p →ₗᵢ[R'] E

`Submodule.subtype` as a `LinearIsometry`.

Equations

- p.subtypeₗᵢ = { toLinearMap := p.subtype, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem Submodule.coe_subtypeₗᵢ {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_11} [Ring R'] [Module R' E] (p : Submodule R' E) :
⇑p.subtypeₗᵢ = ⇑p.subtype
source
@[simp]
theorem Submodule.subtypeₗᵢ_toLinearMap {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_11} [Ring R'] [Module R' E] (p : Submodule R' E) :
p.subtypeₗᵢ.toLinearMap = p.subtype
source
@[simp]
theorem Submodule.subtypeₗᵢ_toContinuousLinearMap {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_11} [Ring R'] [Module R' E] (p : Submodule R' E) :
p.subtypeₗᵢ.toContinuousLinearMap = p.subtypeL
source
structure LinearIsometryEquiv {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] extends E ≃ₛₗ[σ₁₂] E₂ :
Type (max u_11 u_12)

A semilinear isometric equivalence between two normed vector spaces, denoted as `f : E ≃ₛₗᵢ[σ₁₂] E₂`.

- toFun : E → E₂
- map_add' (x y : E) : (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
- map_smul' (m : R) (x : E) : (↑self.toLinearEquiv).toFun (m • x) = σ₁₂ m • (↑self.toLinearEquiv).toFun x
- invFun : E₂ → E
- left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
- right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
- norm_map' (x : E) : ‖self.toLinearEquiv x‖ = ‖x‖

Instances For

source
def «term_≃ₛₗᵢ[_]_» :
Lean.TrailingParserDescr

A semilinear isometric equivalence between two normed vector spaces, denoted as `f : E ≃ₛₗᵢ[σ₁₂] E₂`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def «term_≃ₗᵢ[_]_» :
Lean.TrailingParserDescr

A linear isometric equivalence between two normed vector spaces.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def «term_≃ₗᵢ⋆[_]_» :
Lean.TrailingParserDescr

An antilinear isometric equivalence between two normed vector spaces.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
class SemilinearIsometryEquivClass (𝓕 : Type u_11) {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} [Semiring R] [Semiring R₂] (σ₁₂ : outParam (R →+* R₂)) {σ₂₁ : outParam (R₂ →+* R)} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E : outParam (Type u_14)) (E₂ : outParam (Type u_15)) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [EquivLike 𝓕 E E₂] extends SemilinearEquivClass 𝓕 σ₁₂ E E₂ :
Prop

`SemilinearIsometryEquivClass F σ E E₂` asserts `F` is a type of bundled `σ`-semilinear isometric equivs `E → E₂`.

See also `LinearIsometryEquivClass F R E E₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S` is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and `f (c • x) = (σ c) • f x`.

- map_add (f : 𝓕) (a b : E) : f (a + b) = f a + f b
- map_smulₛₗ (f : 𝓕) (r : R) (x : E) : f (r • x) = σ₁₂ r • f x
- norm_map (f : 𝓕) (x : E) : ‖f x‖ = ‖x‖

Instances

source
@[reducible, inline]
abbrev LinearIsometryEquivClass (𝓕 : Type u_11) (R : outParam (Type u_12)) (E : outParam (Type u_13)) (E₂ : outParam (Type u_14)) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] [EquivLike 𝓕 E E₂] :
Prop

`LinearIsometryEquivClass F R E E₂` asserts `F` is a type of bundled `R`-linear isometries `M → M₂`.

This is an abbreviation for `SemilinearIsometryEquivClass F (RingHom.id R) E E₂`.

Equations

- LinearIsometryEquivClass 𝓕 R E E₂ = SemilinearIsometryEquivClass 𝓕 (RingHom.id R) E E₂

Instances For

source
@[instance 100]
instance SemilinearIsometryEquivClass.toSemilinearIsometryClass {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} (𝓕 : Type u_10) [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [EquivLike 𝓕 E E₂] [s : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂] :
SemilinearIsometryClass 𝓕 σ₁₂ E E₂
source
theorem LinearIsometryEquiv.toLinearEquiv_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Injective toLinearEquiv
source
@[simp]
theorem LinearIsometryEquiv.toLinearEquiv_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
f.toLinearEquiv = g.toLinearEquiv ↔ f = g
source
instance LinearIsometryEquiv.instEquivLike {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
EquivLike (E ≃ₛₗᵢ[σ₁₂] E₂) E E₂
Equations

- One or more equations did not get rendered due to their size.

source
instance LinearIsometryEquiv.instSemilinearIsometryEquivClass {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
source
instance LinearIsometryEquiv.instCoeFun {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
CoeFun (E ≃ₛₗᵢ[σ₁₂] E₂) fun (x : E ≃ₛₗᵢ[σ₁₂] E₂) => E → E₂

Shortcut instance, saving 8.5% of compilation time in `Mathlib/Analysis/InnerProductSpace/Adjoint.lean`.

(This instance was pinpointed by benchmarks; we didn't do an in depth investigation why it is specifically needed.)

Equations

- LinearIsometryEquiv.instCoeFun = { coe := DFunLike.coe }

source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Injective DFunLike.coe
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗ[σ₁₂] E₂) (he : ∀ (x : E), ‖e x‖ = ‖x‖) :
⇑{ toLinearEquiv := e, norm_map' := he } = ⇑e
source
@[simp]
theorem LinearIsometryEquiv.coe_toLinearEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.toLinearEquiv = ⇑e
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {e e' : E ≃ₛₗᵢ[σ₁₂] E₂} (h : ∀ (x : E), e x = e' x) :
e = e'
source
theorem LinearIsometryEquiv.ext_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {e e' : E ≃ₛₗᵢ[σ₁₂] E₂} :
e = e' ↔ ∀ (x : E), e x = e' x
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f : E ≃ₛₗᵢ[σ₁₂] E₂} {x x' : E} :
x = x' → f x = f x'
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} (h : f = g) (x : E) :
f x = g x
source
def LinearIsometryEquiv.ofBounds {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗ[σ₁₂] E₂) (h₁ : ∀ (x : E), ‖e x‖ ≤ ‖x‖) (h₂ : ∀ (y : E₂), ‖e.symm y‖ ≤ ‖y‖) :
E ≃ₛₗᵢ[σ₁₂] E₂

Construct a `LinearIsometryEquiv` from a `LinearEquiv` and two inequalities: `∀ x, ‖e x‖ ≤ ‖x‖` and `∀ y, ‖e.symm y‖ ≤ ‖y‖`.

Equations

- LinearIsometryEquiv.ofBounds e h₁ h₂ = { toLinearEquiv := e, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) :
‖e x‖ = ‖x‖
source
def LinearIsometryEquiv.toLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E →ₛₗᵢ[σ₁₂] E₂

Reinterpret a `LinearIsometryEquiv` as a `LinearIsometry`.

Equations

- e.toLinearIsometry = { toLinearMap := ↑e.toLinearEquiv, norm_map' := ⋯ }

Instances For

source
theorem LinearIsometryEquiv.toLinearIsometry_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Injective toLinearIsometry
source
@[simp]
theorem LinearIsometryEquiv.toLinearIsometry_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
f.toLinearIsometry = g.toLinearIsometry ↔ f = g
source
@[simp]
theorem LinearIsometryEquiv.coe_toLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.toLinearIsometry = ⇑e
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
Isometry ⇑e
source
def LinearIsometryEquiv.toIsometryEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E ≃ᵢ E₂

Reinterpret a `LinearIsometryEquiv` as an `IsometryEquiv`.

Equations

- e.toIsometryEquiv = { toEquiv := e.toEquiv, isometry_toFun := ⋯ }

Instances For

source
theorem LinearIsometryEquiv.toIsometryEquiv_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Injective toIsometryEquiv
source
@[simp]
theorem LinearIsometryEquiv.toIsometryEquiv_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
f.toIsometryEquiv = g.toIsometryEquiv ↔ f = g
source
@[simp]
theorem LinearIsometryEquiv.coe_toIsometryEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.toIsometryEquiv = ⇑e
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
Set.range ⇑e = Set.univ
source
def LinearIsometryEquiv.toHomeomorph {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E ≃ₜ E₂

Reinterpret a `LinearIsometryEquiv` as a `Homeomorph`.

Equations

- e.toHomeomorph = e.toIsometryEquiv.toHomeomorph

Instances For

source
theorem LinearIsometryEquiv.toHomeomorph_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Injective toHomeomorph
source
@[simp]
theorem LinearIsometryEquiv.toHomeomorph_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
f.toHomeomorph = g.toHomeomorph ↔ f = g
source
@[simp]
theorem LinearIsometryEquiv.coe_toHomeomorph {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.toHomeomorph = ⇑e
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
Continuous ⇑e
source
theorem LinearIsometryEquiv.continuousAt {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E} :
ContinuousAt (⇑e) x
source
theorem LinearIsometryEquiv.continuousOn {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {s : Set E} :
ContinuousOn (⇑e) s
source
theorem LinearIsometryEquiv.continuousWithinAt {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {s : Set E} {x : E} :
ContinuousWithinAt (⇑e) s x
source
def LinearIsometryEquiv.toContinuousLinearEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E ≃SL[σ₁₂] E₂

Interpret a `LinearIsometryEquiv` as a `ContinuousLinearEquiv`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem LinearIsometryEquiv.toContinuousLinearEquiv_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Injective toContinuousLinearEquiv
source
@[simp]
theorem LinearIsometryEquiv.toContinuousLinearEquiv_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
f.toContinuousLinearEquiv = g.toContinuousLinearEquiv ↔ f = g
source
@[simp]
theorem LinearIsometryEquiv.coe_toContinuousLinearEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.toContinuousLinearEquiv = ⇑e
source
def LinearIsometryEquiv.refl (R : Type u_1) (E : Type u_5) [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
E ≃ₗᵢ[R] E

Identity map as a `LinearIsometryEquiv`.

Equations

- LinearIsometryEquiv.refl R E = { toLinearEquiv := LinearEquiv.refl R E, norm_map' := ⋯ }

Instances For

source
def LinearIsometryEquiv.ulift (R : Type u_1) (E : Type u_5) [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
ULift.{u_11, u_5} E ≃ₗᵢ[R] E

Linear isometry equiv between a space and its lift to another universe.

Equations

- LinearIsometryEquiv.ulift R E = { toLinearEquiv := ContinuousLinearEquiv.ulift.toLinearEquiv, norm_map' := ⋯ }

Instances For

source
instance LinearIsometryEquiv.instInhabited {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
Inhabited (E ≃ₗᵢ[R] E)
Equations

- LinearIsometryEquiv.instInhabited = { default := LinearIsometryEquiv.refl R E }

source
@[simp]
theorem LinearIsometryEquiv.coe_refl {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
⇑(refl R E) = id
source
def LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E₂ ≃ₛₗᵢ[σ₂₁] E

The inverse `LinearIsometryEquiv`.

Equations

- e.symm = { toLinearEquiv := e.symm, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) :
e (e.symm x) = x
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) :
e.symm (e x) = x
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E} :
e x = 0 ↔ x = 0
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.symm.symm = e
source
theorem LinearIsometryEquiv.symm_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
Function.Bijective symm
source
@[simp]
theorem LinearIsometryEquiv.toLinearEquiv_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.symm.toLinearEquiv = e.symm
source
@[simp]
theorem LinearIsometryEquiv.coe_symm_toLinearEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.symm = ⇑e.symm
source
@[simp]
theorem LinearIsometryEquiv.toContinuousLinearEquiv_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.symm.toContinuousLinearEquiv = e.toContinuousLinearEquiv.symm
source
@[simp]
theorem LinearIsometryEquiv.coe_symm_toContinuousLinearEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.toContinuousLinearEquiv.symm = ⇑e.symm
source
@[simp]
theorem LinearIsometryEquiv.toIsometryEquiv_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.symm.toIsometryEquiv = e.toIsometryEquiv.symm
source
@[simp]
theorem LinearIsometryEquiv.coe_symm_toIsometryEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.toIsometryEquiv.symm = ⇑e.symm
source
@[simp]
theorem LinearIsometryEquiv.toHomeomorph_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.symm.toHomeomorph = e.toHomeomorph.symm
source
@[simp]
theorem LinearIsometryEquiv.coe_symm_toHomeomorph {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.toHomeomorph.symm = ⇑e.symm
source
def LinearIsometryEquiv.Simps.apply {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E ≃ₛₗᵢ[σ₁₂] E₂) :
E → E₂

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

- LinearIsometryEquiv.Simps.apply σ₁₂ E E₂ h = ⇑h

Instances For

source
def LinearIsometryEquiv.Simps.symm_apply {R : Type u_1} {R₂ : Type u_2} [Semiring R] [Semiring R₂] (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E : Type u_11) (E₂ : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E ≃ₛₗᵢ[σ₁₂] E₂) :
E₂ → E

See Note [custom simps projection]

Equations

- LinearIsometryEquiv.Simps.symm_apply σ₁₂ E E₂ h = ⇑h.symm

Instances For

source
def LinearIsometryEquiv.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₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
E ≃ₛₗᵢ[σ₁₃] E₃

Composition of `LinearIsometryEquiv`s as a `LinearIsometryEquiv`.

Equations

- e.trans e' = { toLinearEquiv := e.trans e'.toLinearEquiv, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.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₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
source
@[simp]
theorem LinearIsometryEquiv.trans_apply {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (c : E) :
(e₁.trans e₂) c = e₂ (e₁ c)
source
@[simp]
theorem LinearIsometryEquiv.toLinearEquiv_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₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
(e.trans e').toLinearEquiv = e.trans e'.toLinearEquiv
source
@[simp]
theorem LinearIsometryEquiv.toIsometryEquiv_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₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
(e.trans e').toIsometryEquiv = e.toIsometryEquiv.trans e'.toIsometryEquiv
source
@[simp]
theorem LinearIsometryEquiv.toHomeomorph_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₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
(e.trans e').toHomeomorph = e.toHomeomorph.trans e'.toHomeomorph
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.trans (refl R₂ E₂) = e
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
(refl R E).trans e = e
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.trans e.symm = refl R E
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.symm.trans e = refl R₂ E₂
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e.symm ∘ ⇑e = id
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑e ∘ ⇑e.symm = id
source
@[simp]
theorem LinearIsometryEquiv.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₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
source
theorem LinearIsometryEquiv.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₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R₂ E₂] [Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
⇑(e₁.trans e₂).symm = ⇑e₁.symm ∘ ⇑e₂.symm
source
theorem LinearIsometryEquiv.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₃} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomInvPair σ₁₄ σ₄₁] [RingHomInvPair σ₄₁ σ₁₄] [RingHomInvPair σ₂₄ σ₄₂] [RingHomInvPair σ₄₂ σ₂₄] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₄₂ σ₂₁ σ₄₁] [RingHomCompTriple σ₄₃ σ₃₂ σ₄₂] [RingHomCompTriple σ₄₃ σ₃₁ σ₄₁] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [SeminormedAddCommGroup E₄] [Module R E] [Module R₂ E₂] [Module R₃ E₃] [Module R₄ E₄] (eEE₂ : E ≃ₛₗᵢ[σ₁₂] E₂) (eE₂E₃ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (eE₃E₄ : E₃ ≃ₛₗᵢ[σ₃₄] E₄) :
eEE₂.trans (eE₂E₃.trans eE₃E₄) = (eEE₂.trans eE₂E₃).trans eE₃E₄
source
instance LinearIsometryEquiv.instGroup {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
Group (E ≃ₗᵢ[R] E)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem LinearIsometryEquiv.coe_one {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
⇑1 = id
source
@[simp]
theorem LinearIsometryEquiv.coe_mul {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (e e' : E ≃ₗᵢ[R] E) :
⇑(e * e') = ⇑e ∘ ⇑e'
source
@[simp]
theorem LinearIsometryEquiv.coe_inv {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (e : E ≃ₗᵢ[R] E) :
⇑e⁻¹ = ⇑e.symm
source
theorem LinearIsometryEquiv.one_def {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
1 = refl R E
source
theorem LinearIsometryEquiv.mul_def {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (e e' : E ≃ₗᵢ[R] E) :
e * e' = e'.trans e
source
theorem LinearIsometryEquiv.inv_def {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (e : E ≃ₗᵢ[R] E) :
e⁻¹ = e.symm

Lemmas about mixing the group structure with definitions. Because we have multiple ways to express `LinearIsometryEquiv.refl`, `LinearIsometryEquiv.symm`, and `LinearIsometryEquiv.trans`, we want simp lemmas for every combination. The assumption made here is that if you're using the group structure, you want to preserve it after simp.

This copies the approach used by the lemmas near `Equiv.Perm.trans_one`.

source
@[simp]
theorem LinearIsometryEquiv.trans_one {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.trans 1 = e
source
@[simp]
theorem LinearIsometryEquiv.one_trans {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
trans 1 e = e
source
@[simp]
theorem LinearIsometryEquiv.refl_mul {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (e : E ≃ₗᵢ[R] E) :
refl R E * e = e
source
@[simp]
theorem LinearIsometryEquiv.mul_refl {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (e : E ≃ₗᵢ[R] E) :
e * refl R E = e
source
instance LinearIsometryEquiv.instCoeTCContinuousLinearEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
CoeTC (E ≃ₛₗᵢ[σ₁₂] E₂) (E ≃SL[σ₁₂] E₂)

Reinterpret a `LinearIsometryEquiv` as a `ContinuousLinearEquiv`.

Equations

- LinearIsometryEquiv.instCoeTCContinuousLinearEquiv = { coe := fun (e : E ≃ₛₗᵢ[σ₁₂] E₂) => { toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } }

source
instance LinearIsometryEquiv.instCoeTCContinuousLinearMap {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] :
CoeTC (E ≃ₛₗᵢ[σ₁₂] E₂) (E →SL[σ₁₂] E₂)
Equations

- LinearIsometryEquiv.instCoeTCContinuousLinearMap = { coe := fun (e : E ≃ₛₗᵢ[σ₁₂] E₂) => ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } }

source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ⇑e
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ⇑e
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e 0 = 0
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E) :
e (x + y) = e x + e y
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E) :
e (x - y) = e x - e y
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (c : R) (x : E) :
e (c • x) = σ₁₂ c • e x
source
theorem LinearIsometryEquiv.map_smul {R : Type u_1} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E) :
e (c • x) = c • e x
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) :
‖e x‖₊ = ‖x‖₊
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E) :
dist (e x) (e y) = dist x y
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E) :
edist (e x) (e y) = edist x y
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
Function.Bijective ⇑e
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
Function.Injective ⇑e
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
Function.Surjective ⇑e
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x y : E} :
e x = e y ↔ x = y
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x y : E} (h : x ≠ y) :
e x ≠ e y
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
LipschitzWith 1 ⇑e
source
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) :
AntilipschitzWith 1 ⇑e
source
theorem LinearIsometryEquiv.image_eq_preimage_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
⇑e '' s = ⇑e.symm ⁻¹' s
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
EMetric.diam (⇑e '' s) = EMetric.diam s
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : Set E) :
Metric.diam (⇑e '' s) = Metric.diam s
source
@[simp]
theorem LinearIsometryEquiv.preimage_ball {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) (r : ℝ) :
⇑e ⁻¹' Metric.ball x r = Metric.ball (e.symm x) r
source
@[simp]
theorem LinearIsometryEquiv.preimage_sphere {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) (r : ℝ) :
⇑e ⁻¹' Metric.sphere x r = Metric.sphere (e.symm x) r
source
@[simp]
theorem LinearIsometryEquiv.preimage_closedBall {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) (r : ℝ) :
⇑e ⁻¹' Metric.closedBall x r = Metric.closedBall (e.symm x) r
source
@[simp]
theorem LinearIsometryEquiv.image_ball {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ) :
⇑e '' Metric.ball x r = Metric.ball (e x) r
source
@[simp]
theorem LinearIsometryEquiv.image_sphere {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ) :
⇑e '' Metric.sphere x r = Metric.sphere (e x) r
source
@[simp]
theorem LinearIsometryEquiv.image_closedBall {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ) :
⇑e '' Metric.closedBall x r = Metric.closedBall (e x) r
source
@[simp]
theorem LinearIsometryEquiv.comp_continuousOn_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {α : Type u_11} [TopologicalSpace α] {f : α → E} {s : Set α} :
ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s
source
@[simp]
theorem LinearIsometryEquiv.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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) {α : Type u_11} [TopologicalSpace α] {f : α → E} :
Continuous (⇑e ∘ f) ↔ Continuous f
source
instance LinearIsometryEquiv.completeSpace_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (p : Submodule R E) [CompleteSpace ↥p] :
CompleteSpace ↥(Submodule.map (↑e.toLinearEquiv) p)
source
noncomputable def LinearIsometryEquiv.ofSurjective {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective ⇑f) :
F ≃ₛₗᵢ[σ₁₂] E₂

Construct a linear isometry equiv from a surjective linear isometry.

Equations

- LinearIsometryEquiv.ofSurjective f hfr = { toLinearEquiv := LinearEquiv.ofBijective f.toLinearMap ⋯, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.coe_ofSurjective {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E₂] [Module R₂ E₂] [NormedAddCommGroup F] [Module R F] (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective ⇑f) :
⇑(ofSurjective f hfr) = ⇑f
source
def LinearIsometryEquiv.ofLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ f.toLinearMap = LinearMap.id) :
E ≃ₛₗᵢ[σ₁₂] E₂

If a linear isometry has an inverse, it is a linear isometric equivalence.

Equations

- LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂ = { toLinearEquiv := LinearEquiv.ofLinear f.toLinearMap g h₁ h₂, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.coe_ofLinearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ f.toLinearMap = LinearMap.id) :
⇑(ofLinearIsometry f g h₁ h₂) = ⇑f
source
@[simp]
theorem LinearIsometryEquiv.coe_ofLinearIsometry_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} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ f.toLinearMap = LinearMap.id) :
⇑(ofLinearIsometry f g h₁ h₂).symm = ⇑g
source
def LinearIsometryEquiv.neg (R : Type u_1) {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
E ≃ₗᵢ[R] E

The negation operation on a normed space `E`, considered as a linear isometry equivalence.

Equations

- LinearIsometryEquiv.neg R = { toLinearEquiv := LinearEquiv.neg R, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.coe_neg {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
⇑(neg R) = fun (x : E) => -x
source
@[simp]
theorem LinearIsometryEquiv.symm_neg {R : Type u_1} {E : Type u_5} [Semiring R] [SeminormedAddCommGroup E] [Module R E] :
(neg R).symm = neg R
source
def LinearIsometryEquiv.prodComm (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] :
E × E₂ ≃ₗᵢ[R] E₂ × E

The natural equivalence `E × E₂ ≃ E₂ × E` is a linear isometry.

Equations

- LinearIsometryEquiv.prodComm R E E₂ = { toLinearEquiv := LinearEquiv.prodComm R E E₂, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.prodComm_symm_apply (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] (a✝ : E₂ × E) :
(prodComm R E E₂).symm a✝ = a✝.swap
source
@[simp]
theorem LinearIsometryEquiv.prodComm_apply (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] (a✝ : E × E₂) :
(prodComm R E E₂) a✝ = a✝.swap
source
@[simp]
theorem LinearIsometryEquiv.symm_prodComm (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] :
(prodComm R E E₂).symm = prodComm R E₂ E
source
def LinearIsometryEquiv.prodAssoc (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R E₂] [Module R E₃] :
(E × E₂) × E₃ ≃ₗᵢ[R] E × E₂ × E₃

The natural equivalence `(E × E₂) × E₃ ≃ E × (E₂ × E₃)` is a linear isometry.

Equations

- LinearIsometryEquiv.prodAssoc R E E₂ E₃ = { toLinearEquiv := LinearEquiv.prodAssoc R E E₂ E₃, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.coe_prodAssoc (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R E₂] [Module R E₃] :
⇑(prodAssoc R E E₂ E₃) = ⇑(Equiv.prodAssoc E E₂ E₃)
source
@[simp]
theorem LinearIsometryEquiv.coe_prodAssoc_symm (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [SeminormedAddCommGroup E₃] [Module R E] [Module R E₂] [Module R E₃] :
⇑(prodAssoc R E E₂ E₃).symm = ⇑(Equiv.prodAssoc E E₂ E₃).symm
source
def LinearIsometryEquiv.ofTop (E : Type u_5) [SeminormedAddCommGroup E] {R : Type u_12} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ⊤) :
↥p ≃ₗᵢ[R] E

If `p` is a submodule that is equal to `⊤`, then `LinearIsometryEquiv.ofTop p hp` is the "identity" equivalence between `p` and `E`.

Equations

- LinearIsometryEquiv.ofTop E p hp = { toLinearEquiv := LinearEquiv.ofTop p hp, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.ofTop_toLinearEquiv (E : Type u_5) [SeminormedAddCommGroup E] {R : Type u_12} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ⊤) :
(ofTop E p hp).toLinearEquiv = LinearEquiv.ofTop p hp
source
@[simp]
theorem LinearIsometryEquiv.ofTop_apply (E : Type u_5) [SeminormedAddCommGroup E] {R : Type u_12} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ⊤) (self : ↥p) :
(ofTop E p hp) self = ↑self
source
@[simp]
theorem LinearIsometryEquiv.ofTop_symm_apply_coe (E : Type u_5) [SeminormedAddCommGroup E] {R : Type u_12} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ⊤) (x : E) :
↑((ofTop E p hp).symm x) = x
source
def LinearIsometryEquiv.ofEq {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_12} [Ring R'] [Module R' E] (p q : Submodule R' E) (hpq : p = q) :
↥p ≃ₗᵢ[R'] ↥q

`LinearEquiv.ofEq` as a `LinearIsometryEquiv`.

Equations

- LinearIsometryEquiv.ofEq p q hpq = { toLinearEquiv := LinearEquiv.ofEq p q hpq, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.coe_ofEq_apply {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_12} [Ring R'] [Module R' E] {p q : Submodule R' E} (h : p = q) (x : ↥p) :
↑((ofEq p q h) x) = ↑x
source
@[simp]
theorem LinearIsometryEquiv.ofEq_symm {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_12} [Ring R'] [Module R' E] {p q : Submodule R' E} (h : p = q) :
(ofEq p q h).symm = ofEq q p ⋯
source
@[simp]
theorem LinearIsometryEquiv.ofEq_rfl {E : Type u_5} [SeminormedAddCommGroup E] {R' : Type u_12} [Ring R'] [Module R' E] {p : Submodule R' E} :
ofEq p p ⋯ = refl R' ↥p
source
def LinearIsometryEquiv.submoduleMap {R : Type u_13} {R₂ : Type u_15} {M : Type u_16} {M₂ : Type u_17} [Ring R] [Ring R₂] [SeminormedAddCommGroup M] [SeminormedAddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : Submodule R M) (e : M ≃ₛₗᵢ[σ₁₂] M₂) :
↥p ≃ₛₗᵢ[σ₁₂] ↥(Submodule.map e p)

A linear isometry equivalence between two modules restricts to a linear isometry equivalence from any submodule `p` of the domain onto the image of that submodule.

This is a version of `LinearEquiv.submoduleMap` extended to linear isometry equivalences.

Equations

- LinearIsometryEquiv.submoduleMap p e = { toLinearEquiv := e.submoduleMap p, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.submoduleMap_symm_apply_coe {R : Type u_13} {R₂ : Type u_15} {M : Type u_16} {M₂ : Type u_17} [Ring R] [Ring R₂] [SeminormedAddCommGroup M] [SeminormedAddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : Submodule R M) (e : M ≃ₛₗᵢ[σ₁₂] M₂) (y : ↥(Submodule.map (↑e.toLinearEquiv) p)) :
↑((submoduleMap p e).symm y) = e.symm ↑y
source
@[simp]
theorem LinearIsometryEquiv.submoduleMap_apply_coe {R : Type u_13} {R₂ : Type u_15} {M : Type u_16} {M₂ : Type u_17} [Ring R] [Ring R₂] [SeminormedAddCommGroup M] [SeminormedAddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : Submodule R M) (e : M ≃ₛₗᵢ[σ₁₂] M₂) (c : ↥p) :
↑((submoduleMap p e) c) = e ↑c
source
theorem Module.Basis.ext_linearIsometry {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {ι : Type u_11} (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.

source
theorem Module.Basis.ext_linearIsometryEquiv {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] {ι : Type u_11} (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.

source
noncomputable def LinearIsometry.equivRange {E : Type u_5} {F : Type u_9} [SeminormedAddCommGroup E] [NormedAddCommGroup F] {R : Type u_11} {S : Type u_12} [Semiring R] [Ring S] [Module S E] [Module R F] {σ₁₂ : R →+* S} {σ₂₁ : S →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : F →ₛₗᵢ[σ₁₂] E) :
F ≃ₛₗᵢ[σ₁₂] ↥(LinearMap.range f.toLinearMap)

Reinterpret a `LinearIsometry` as a `LinearIsometryEquiv` to the range.

Equations

- f.equivRange = { toLinearEquiv := LinearEquiv.ofInjective f.toLinearMap ⋯, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometry.equivRange_apply_coe {E : Type u_5} {F : Type u_9} [SeminormedAddCommGroup E] [NormedAddCommGroup F] {R : Type u_11} {S : Type u_12} [Semiring R] [Ring S] [Module S E] [Module R F] {σ₁₂ : R →+* S} {σ₂₁ : S →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : F →ₛₗᵢ[σ₁₂] E) (a : F) :
↑(f.equivRange a) = f a
source
theorem MulOpposite.isometry_opLinearEquiv {R : Type u_11} {H : Type u_12} [Semiring R] [SeminormedAddCommGroup H] [Module R H] :
Isometry ⇑(opLinearEquiv R)
source
def MulOpposite.opLinearIsometryEquiv (R : Type u_11) (H : Type u_12) [Semiring R] [SeminormedAddCommGroup H] [Module R H] :
H ≃ₗᵢ[R] H ᵐᵒᵖ

The linear isometry equivalence version of the function `op`.

Equations

- MulOpposite.opLinearIsometryEquiv R H = { toLinearEquiv := MulOpposite.opLinearEquiv R, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem MulOpposite.opLinearIsometryEquiv_apply (R : Type u_11) (H : Type u_12) [Semiring R] [SeminormedAddCommGroup H] [Module R H] (a✝ : H) :
(opLinearIsometryEquiv R H) a✝ = op a✝
source
@[simp]
theorem MulOpposite.opLinearIsometryEquiv_symm_apply (R : Type u_11) (H : Type u_12) [Semiring R] [SeminormedAddCommGroup H] [Module R H] (a✝ : H ᵐᵒᵖ) :
(opLinearIsometryEquiv R H).symm a✝ = unop a✝
source
@[simp]
theorem MulOpposite.toLinearEquiv_opLinearIsometryEquiv {R : Type u_11} {H : Type u_12} [Semiring R] [SeminormedAddCommGroup H] [Module R H] :
(opLinearIsometryEquiv R H).toLinearEquiv = opLinearEquiv R
source
@[simp]
theorem MulOpposite.toContinuousLinearEquiv_opLinearIsometryEquiv {R : Type u_11} {H : Type u_12} [Semiring R] [SeminormedAddCommGroup H] [Module R H] :
(opLinearIsometryEquiv R H).toContinuousLinearEquiv = opContinuousLinearEquiv R