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

• e.toContinuousAffineMap: the continuous affine equivalence e as a continuous affine map

• 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₁ ≃ᴬ[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_≃ᴬ[_]_» : Lean.TrailingParserDescr

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

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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : P₁ ≃ₜ P₂

A continuous affine equivalence is a homeomorphism.

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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : Function.Injective toAffineEquiv

@[implicit_reducible]

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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : EquivLike (P₁ ≃ᴬ[k] P₂) P₁ P₂

instance ContinuousAffineEquiv.instHomeomorphClass {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : HomeomorphClass (P₁ ≃ᴬ[k] P₂) P₁ P₂

@[implicit_reducible]

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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : Coe (P₁ ≃ᴬ[k] P₂) (P₁ ≃ᵃ[k] P₂)

Coerce continuous affine equivalences to affine equivalences.

@[implicit_reducible]

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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : FunLike (P₁ ≃ᴬ[k] P₂) P₁ P₂

@[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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.

def ContinuousAffineEquiv.Simps.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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : P₂ → P₁

See Note [custom simps projection].

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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] {e e' : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] {e e' : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : Continuous ⇑e

def ContinuousAffineEquiv.toContinuousAffineMap {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : P₁ →ᴬ[k] P₂

A continuous affine equivalence is a continuous affine map.

@[implicit_reducible]

instance ContinuousAffineEquiv.ContinuousAffineMap.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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : Coe (P₁ ≃ᴬ[k] P₂) (P₁ →ᴬ[k] P₂)

Coerce continuous linear equivs to continuous linear maps.

@[simp]

theorem ContinuousAffineEquiv.coe_toContinuousAffineMap {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : ⇑e.toContinuousAffineMap = ⇑e

theorem ContinuousAffineEquiv.toContinuousAffineMap_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : Function.Injective toContinuousAffineMap

theorem ContinuousAffineEquiv.toContinuousAffineMap_toAffineMap {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : ↑e.toContinuousAffineMap = ↑↑e

theorem ContinuousAffineEquiv.toContinuousAffineMap_toContinuousMap {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : e.toContinuousAffineMap.toContinuousMap = ↑e.toHomeomorph

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₁ ≃ᴬ[k] P₁

Identity map as a ContinuousAffineEquiv.

@[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₁] : ⇑(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₁) : (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₁] : ↑(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₁] : (↑(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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : P₂ ≃ᴬ[k] P₁

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

@[simp]

theorem ContinuousAffineEquiv.toAffineEquiv_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : ↑e.symm = (↑e).symm

@[simp]

theorem ContinuousAffineEquiv.coe_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : ⇑(↑e).symm = ⇑e.symm

@[simp]

theorem ContinuousAffineEquiv.toEquiv_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : (↑e.symm).toEquiv = (↑e).symm

@[simp]

theorem ContinuousAffineEquiv.coe_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : ⇑(↑e).symm = ⇑e.symm

@[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : e.symm.symm = e

theorem ContinuousAffineEquiv.symm_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : Function.Bijective symm

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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (f : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (f : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : Function.Injective ⇑e

theorem ContinuousAffineEquiv.image_eq_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[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₁] : (refl k P₁).symm = 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₁] : (refl k P₁).symm = 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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[k] P₃) : P₁ ≃ᴬ[k] P₃

Composition of two ContinuousAffineEquivalences, applied left to right.

@[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₂ ≃ᴬ[k] P₃) (e₃ : P₃ ≃ᴬ[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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : e.trans (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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : (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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : e.trans e.symm = 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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) : e.symm.trans e = refl k P₂

theorem ContinuousAffineEquiv.trans_toContinuousAffineMap {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[k] P₃) : (e.trans e').toContinuousAffineMap = e'.toContinuousAffineMap.comp e.toContinuousAffineMap

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 ≃ᴬ[k] F

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

@[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

theorem ContinuousLinearEquiv.toContinuousAffineEquiv_toContinuousAffineMap {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) : L.toContinuousAffineEquiv.toContinuousAffineMap = (↑L).toContinuousAffineMap

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₁ ≃ᴬ[k] P₁

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

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₁) : ↑(constVAdd k P₁ v) = AffineEquiv.constVAdd k P₁ v

def ContinuousAffineEquiv.prodCongr {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₃ ≃ᴬ[k] P₄) : P₁ × P₃ ≃ᴬ[k] P₂ × P₄

Product of two continuous affine equivalences. The map comes from Equiv.prodCongr

@[simp]

theorem ContinuousAffineEquiv.prodCongr_toAffineEquiv {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₃ ≃ᴬ[k] P₄) : ↑(e₁.prodCongr e₂) = (↑e₁).prodCongr ↑e₂

@[simp]

theorem ContinuousAffineEquiv.prodCongr_symm {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₃ ≃ᴬ[k] P₄) : (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm

@[simp]

theorem ContinuousAffineEquiv.prodCongr_apply {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₃ ≃ᴬ[k] P₄) (p : P₁ × P₃) : (e₁.prodCongr e₂) p = (e₁ p.1, e₂ p.2)

@[simp]

theorem ContinuousAffineEquiv.prodCongr_toContinuousAffineMap {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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₃ ≃ᴬ[k] P₄) : (e₁.prodCongr e₂).toContinuousAffineMap = e₁.toContinuousAffineMap.prodMap e₂.toContinuousAffineMap

def ContinuousAffineEquiv.prodComm (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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : P₁ × P₂ ≃ᴬ[k] P₂ × P₁

Product of affine spaces is commutative up to continuous affine isomorphism.

@[simp]

theorem ContinuousAffineEquiv.prodComm_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (a✝ : P₁ × P₂) : (prodComm k P₁ P₂) a✝ = a✝.swap

@[simp]

theorem ContinuousAffineEquiv.prodComm_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (a✝ : P₂ × P₁) : (↑(prodComm k P₁ P₂)).symm a✝ = a✝.swap

@[simp]

theorem ContinuousAffineEquiv.prodComm_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : ↑(prodComm k P₁ P₂) = AffineEquiv.prodComm k P₁ P₂

@[simp]

theorem ContinuousAffineEquiv.prodComm_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] : (prodComm k P₁ P₂).symm = prodComm k P₂ P₁

def ContinuousAffineEquiv.prodAssoc (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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] : (P₁ × P₂) × P₃ ≃ᴬ[k] P₁ × P₂ × P₃

Product of affine spaces is associative up to continuous affine isomorphism.

@[simp]

theorem ContinuousAffineEquiv.prodAssoc_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (p : (P₁ × P₂) × P₃) : (prodAssoc k P₁ P₂ P₃) p = (p.1.1, p.1.2, p.2)

@[simp]

theorem ContinuousAffineEquiv.prodAssoc_toAffineEquiv (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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] : ↑(prodAssoc k P₁ P₂ P₃) = AffineEquiv.prodAssoc k P₁ P₂ P₃

@[simp]

theorem ContinuousAffineEquiv.prodAssoc_symm_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₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (p : P₁ × P₂ × P₃) : (↑(prodAssoc k P₁ P₂ P₃)).symm p = ((p.1, p.2.1), p.2.2)