Continuous affine equivalences

In this file, we define continuous affine equivalences, affine equivalences which are continuous with continuous inverse.

Main definitions

• ContinuousAffineEquiv.refl k P: the identity map as a ContinuousAffineEquiv;

• e.symm: the inverse map of a ContinuousAffineEquiv as a ContinuousAffineEquiv;

• e.trans e': composition of two ContinuousAffineEquivs; note that the order follows mathlib's CategoryTheory convention (apply e, then e'), not the convention used in function composition and compositions of bundled morphisms.

• e.toHomeomorph: the continuous affine equivalence e as a homeomorphism

• ContinuousLinearEquiv.toContinuousAffineEquiv: a continuous linear equivalence as a continuous affine equivalence

• ContinuousAffineEquiv.constVAdd: AffineEquiv.constVAdd as a continuous affine equivalence

TODO

• equip ContinuousAffineEquiv k P P with a Group structure, with multiplication corresponding to composition in AffineEquiv.group.

structure ContinuousAffineEquiv (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_4} {V₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] extends P₁ ≃ᵃ[k] P₂ : Type (max (max (max u_2 u_3) u_4) u_5)

A continuous affine equivalence, denoted P₁ ≃ᵃL[k] P₂, between two affine topological spaces is an affine equivalence such that forward and inverse maps are continuous.

• toFun : P₁ → P₂
• invFun : P₂ → P₁
• left_inv : Function.LeftInverse (↑self).invFun (↑self).toFun
• right_inv : Function.RightInverse (↑self).invFun (↑self).toFun
• linear : V₁ ≃ₗ[k] V₂
• map_vadd' (p : P₁) (v : V₁) : (↑self).toEquiv (v +ᵥ p) = (↑self).linear v +ᵥ (↑self).toEquiv p
• continuous_toFun : Continuous (↑self).toFun
• continuous_invFun : Continuous (↑self).invFun

def «term_≃ᵃL[_]_» : Lean.TrailingParserDescr

A continuous affine equivalence, denoted P₁ ≃ᵃL[k] P₂, between two affine topological spaces is an affine equivalence such that forward and inverse maps are continuous.

Equations

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

def ContinuousAffineEquiv.toHomeomorph {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : P₁ ≃ₜ P₂

A continuous affine equivalence is a homeomorphism.

Equations

• e.toHomeomorph = { toEquiv := (↑e).toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem ContinuousAffineEquiv.toAffineEquiv_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] : Function.Injective ContinuousAffineEquiv.toAffineEquiv

instance ContinuousAffineEquiv.instEquivLike {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] : EquivLike (P₁ ≃ᵃL[k] P₂) P₁ P₂

Equations

• ContinuousAffineEquiv.instEquivLike = { coe := fun (f : P₁ ≃ᵃL[k] P₂) => (↑f).toFun, inv := fun (f : P₁ ≃ᵃL[k] P₂) => (↑f).invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance ContinuousAffineEquiv.coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] : Coe (P₁ ≃ᵃL[k] P₂) (P₁ ≃ᵃ[k] P₂)

Coerce continuous affine equivalences to affine equivalences.

Equations

• ContinuousAffineEquiv.coe = { coe := ContinuousAffineEquiv.toAffineEquiv }

theorem ContinuousAffineEquiv.coe_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] : Function.Injective ContinuousAffineEquiv.toAffineEquiv

instance ContinuousAffineEquiv.instFunLike {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] : FunLike (P₁ ≃ᵃL[k] P₂) P₁ P₂

Equations

• ContinuousAffineEquiv.instFunLike = { coe := fun (f : P₁ ≃ᵃL[k] P₂) => ⇑↑f, coe_injective' := ⋯ }

@[simp]

theorem ContinuousAffineEquiv.coe_coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : ⇑↑e = ⇑e

@[simp]

theorem ContinuousAffineEquiv.coe_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : ⇑(↑e).toEquiv = ⇑e

def ContinuousAffineEquiv.Simps.apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : P₁ → P₂

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

Equations

• ContinuousAffineEquiv.Simps.apply e = ⇑e

def ContinuousAffineEquiv.Simps.coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : P₁ ≃ᵃ[k] P₂

See Note [custom simps projection].

Equations

• ContinuousAffineEquiv.Simps.coe e = ↑e

theorem ContinuousAffineEquiv.ext {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] {e e' : P₁ ≃ᵃL[k] P₂} (h : ∀ (x : P₁), e x = e' x) : e = e'

theorem ContinuousAffineEquiv.continuous {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : Continuous ⇑e

def ContinuousAffineEquiv.refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] : P₁ ≃ᵃL[k] P₁

Identity map as a ContinuousAffineEquiv.

Equations

• ContinuousAffineEquiv.refl k P₁ = { toEquiv := Equiv.refl P₁, linear := LinearEquiv.refl k V₁, map_vadd' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousAffineEquiv.coe_refl {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] : ⇑(ContinuousAffineEquiv.refl k P₁) = id

@[simp]

theorem ContinuousAffineEquiv.refl_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] (x : P₁) : (ContinuousAffineEquiv.refl k P₁) x = x

@[simp]

theorem ContinuousAffineEquiv.toAffineEquiv_refl {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] : ↑(ContinuousAffineEquiv.refl k P₁) = AffineEquiv.refl k P₁

@[simp]

theorem ContinuousAffineEquiv.toEquiv_refl {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] : (↑(ContinuousAffineEquiv.refl k P₁)).toEquiv = Equiv.refl P₁

def ContinuousAffineEquiv.symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : P₂ ≃ᵃL[k] P₁

Inverse of a continuous affine equivalence as a continuous affine equivalence.

Equations

• e.symm = { toAffineEquiv := (↑e).symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousAffineEquiv.symm_toAffineEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : (↑e).symm = ↑e.symm

@[simp]

theorem ContinuousAffineEquiv.symm_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : (↑e).symm = (↑e.symm).toEquiv

@[simp]

theorem ContinuousAffineEquiv.apply_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (p : P₂) : e (e.symm p) = p

@[simp]

theorem ContinuousAffineEquiv.symm_apply_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (p : P₁) : e.symm (e p) = p

theorem ContinuousAffineEquiv.apply_eq_iff_eq_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) {p₁ : P₁} {p₂ : P₂} : e p₁ = p₂ ↔ p₁ = e.symm p₂

theorem ContinuousAffineEquiv.apply_eq_iff_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) {p₁ p₂ : P₁} : e p₁ = e p₂ ↔ p₁ = p₂

@[simp]

theorem ContinuousAffineEquiv.symm_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : e.symm.symm = e

theorem ContinuousAffineEquiv.symm_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (x : P₁) : e.symm.symm x = e x

theorem ContinuousAffineEquiv.symm_apply_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) {x : P₂} {y : P₁} : e.symm x = y ↔ x = e y

theorem ContinuousAffineEquiv.eq_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) {x : P₂} {y : P₁} : y = e.symm x ↔ e y = x

@[simp]

theorem ContinuousAffineEquiv.image_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (f : P₁ ≃ᵃL[k] P₂) (s : Set P₂) : ⇑f.symm '' s = ⇑f ⁻¹' s

@[simp]

theorem ContinuousAffineEquiv.preimage_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (f : P₁ ≃ᵃL[k] P₂) (s : Set P₁) : ⇑f.symm ⁻¹' s = ⇑f '' s

theorem ContinuousAffineEquiv.bijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : Function.Bijective ⇑e

theorem ContinuousAffineEquiv.surjective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : Function.Surjective ⇑e

theorem ContinuousAffineEquiv.injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : Function.Injective ⇑e

theorem ContinuousAffineEquiv.image_eq_preimage {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₁) : ⇑e '' s = ⇑e.symm ⁻¹' s

theorem ContinuousAffineEquiv.image_symm_eq_preimage {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₂) : ⇑e.symm '' s = ⇑e ⁻¹' s

@[simp]

theorem ContinuousAffineEquiv.image_preimage {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₂) : ⇑e '' (⇑e ⁻¹' s) = s

@[simp]

theorem ContinuousAffineEquiv.preimage_image {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₁) : ⇑e ⁻¹' (⇑e '' s) = s

theorem ContinuousAffineEquiv.symm_image_image {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₁) : ⇑e.symm '' (⇑e '' s) = s

theorem ContinuousAffineEquiv.image_symm_image {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₂) : ⇑e '' (⇑e.symm '' s) = s

@[simp]

theorem ContinuousAffineEquiv.refl_symm {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] : (ContinuousAffineEquiv.refl k P₁).symm = ContinuousAffineEquiv.refl k P₁

@[simp]

theorem ContinuousAffineEquiv.symm_refl {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] : (ContinuousAffineEquiv.refl k P₁).symm = ContinuousAffineEquiv.refl k P₁

def ContinuousAffineEquiv.trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₁] [TopologicalSpace P₂] [TopologicalSpace P₃] (e : P₁ ≃ᵃL[k] P₂) (e' : P₂ ≃ᵃL[k] P₃) : P₁ ≃ᵃL[k] P₃

Composition of two ContinuousAffineEquivalences, applied left to right.

Equations

• e.trans e' = { toAffineEquiv := (↑e).trans ↑e', continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousAffineEquiv.coe_trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₁] [TopologicalSpace P₂] [TopologicalSpace P₃] (e : P₁ ≃ᵃL[k] P₂) (e' : P₂ ≃ᵃL[k] P₃) : ⇑(e.trans e') = ⇑e' ∘ ⇑e

@[simp]

theorem ContinuousAffineEquiv.trans_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₁] [TopologicalSpace P₂] [TopologicalSpace P₃] (e : P₁ ≃ᵃL[k] P₂) (e' : P₂ ≃ᵃL[k] P₃) (p : P₁) : (e.trans e') p = e' (e p)

theorem ContinuousAffineEquiv.trans_assoc {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} {V₄ : Type u_9} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₁] [TopologicalSpace P₂] [TopologicalSpace P₃] [TopologicalSpace P₄] (e₁ : P₁ ≃ᵃL[k] P₂) (e₂ : P₂ ≃ᵃL[k] P₃) (e₃ : P₃ ≃ᵃL[k] P₄) : (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)

@[simp]

theorem ContinuousAffineEquiv.trans_refl {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : e.trans (ContinuousAffineEquiv.refl k P₂) = e

@[simp]

theorem ContinuousAffineEquiv.refl_trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : (ContinuousAffineEquiv.refl k P₁).trans e = e

@[simp]

theorem ContinuousAffineEquiv.self_trans_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : e.trans e.symm = ContinuousAffineEquiv.refl k P₁

@[simp]

theorem ContinuousAffineEquiv.symm_trans_self {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) : e.symm.trans e = ContinuousAffineEquiv.refl k P₂

def ContinuousLinearEquiv.toContinuousAffineEquiv {k : Type u_1} [Ring k] {E : Type u_10} {F : Type u_11} [AddCommGroup E] [Module k E] [TopologicalSpace E] [AddCommGroup F] [Module k F] [TopologicalSpace F] (L : E ≃L[k] F) : E ≃ᵃL[k] F

Reinterpret a continuous linear equivalence between modules as a continuous affine equivalence.

Equations

• L.toContinuousAffineEquiv = { toAffineEquiv := L.toAffineEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.coe_toContinuousAffineEquiv {k : Type u_1} [Ring k] {E : Type u_10} {F : Type u_11} [AddCommGroup E] [Module k E] [TopologicalSpace E] [AddCommGroup F] [Module k F] [TopologicalSpace F] (e : E ≃L[k] F) : ⇑e.toContinuousAffineEquiv = ⇑e

def ContinuousAffineEquiv.constVAdd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [ContinuousConstVAdd V₁ P₁] (v : V₁) : P₁ ≃ᵃL[k] P₁

The map p ↦ v +ᵥ p as a continuous affine automorphism of an affine space on which addition is continuous.

Equations

• ContinuousAffineEquiv.constVAdd k P₁ v = { toAffineEquiv := AffineEquiv.constVAdd k P₁ v, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem ContinuousAffineEquiv.constVAdd_coe {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [ContinuousConstVAdd V₁ P₁] (v : V₁) : ↑(ContinuousAffineEquiv.constVAdd k P₁ v) = AffineEquiv.constVAdd k P₁ v