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

• ContinuousAffineEquiv.toHomeomorph e = let __spread.0 := e; { toEquiv := __spread.0.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.instCoeFunContinuousAffineEquivForAll {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₂] : CoeFun (P₁ ≃ᵃL[k] P₂) fun (x : P₁ ≃ᵃL[k] P₂) => P₁ → P₂

Equations

• ContinuousAffineEquiv.instCoeFunContinuousAffineEquivForAll = DFunLike.hasCoeToFun

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 : P₁ ≃ᵃL[k] P₂} {e' : P₁ ≃ᵃL[k] P₂} (h : ∀ (x : P₁), e x = e' x) : e = e'

theorem ContinuousAffineEquiv.ext_iff {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' : P₁ ≃ᵃL[k] P₂} : e = e' ↔ ∀ (x : P₁), e x = e' x

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₁ = { toAffineEquiv := { 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

• ContinuousAffineEquiv.symm e = { toAffineEquiv := AffineEquiv.symm ↑e, 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₂) : AffineEquiv.symm ↑e = ↑(ContinuousAffineEquiv.symm e)

@[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 = (ContinuousAffineEquiv.symm e).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 ((ContinuousAffineEquiv.symm e) 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₁) : (ContinuousAffineEquiv.symm e) (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₁ = (ContinuousAffineEquiv.symm e) 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₂ : 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₂) : ContinuousAffineEquiv.symm (ContinuousAffineEquiv.symm e) = 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₁) : (ContinuousAffineEquiv.symm (ContinuousAffineEquiv.symm e)) 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₁} : (ContinuousAffineEquiv.symm e) 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 = (ContinuousAffineEquiv.symm e) 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₂) : ⇑(ContinuousAffineEquiv.symm f) '' 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₁) : ⇑(ContinuousAffineEquiv.symm f) ⁻¹' 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 = ⇑(ContinuousAffineEquiv.symm e) ⁻¹' 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₂) : ⇑(ContinuousAffineEquiv.symm e) '' 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₁) : ⇑(ContinuousAffineEquiv.symm e) '' (⇑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 '' (⇑(ContinuousAffineEquiv.symm e) '' 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.symm (ContinuousAffineEquiv.refl k P₁) = 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.symm (ContinuousAffineEquiv.refl k P₁) = 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

• ContinuousAffineEquiv.trans e e' = { toAffineEquiv := AffineEquiv.trans ↑e ↑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₃) : ⇑(ContinuousAffineEquiv.trans e 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₁) : (ContinuousAffineEquiv.trans e 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₄) : ContinuousAffineEquiv.trans (ContinuousAffineEquiv.trans e₁ e₂) e₃ = ContinuousAffineEquiv.trans e₁ (ContinuousAffineEquiv.trans e₂ 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₂) : ContinuousAffineEquiv.trans e (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.trans (ContinuousAffineEquiv.refl k P₁) 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₂) : ContinuousAffineEquiv.trans e (ContinuousAffineEquiv.symm e) = 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₂) : ContinuousAffineEquiv.trans (ContinuousAffineEquiv.symm e) 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

• ContinuousLinearEquiv.toContinuousAffineEquiv L = { toAffineEquiv := LinearEquiv.toAffineEquiv L.toLinearEquiv, 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) : ⇑(ContinuousLinearEquiv.toContinuousAffineEquiv e) = ⇑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