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.

source

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

Instances For

source

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.

Equations

Instances For

source

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.

Equations

Instances For

source

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

source

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₂

Equations

source

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.

Equations

source

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

Function.Injective toAffineEquiv

source

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₂

Equations

source

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

source

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

source

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.

Equations

Instances For

source

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].

Equations

Instances For

source

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'

source

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

source

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

source

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.

Equations

Instances For

source

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

source

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

source

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

source

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

source

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.

Equations

Instances For

source

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

source

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

source

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

source

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

source

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.

Equations

Instances For

source

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

source

@[deprecated "use instead `toAffineEquiv_symm`, in the reverse direction" (since := "2025-06-08")]

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

(↑e).symm = ↑e.symm

source

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

source

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

source

@[deprecated "use instead `symm_toEquiv`, in the reverse direction" (since := "2025-06-08")]

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

(↑e).symm = (↑e.symm).toEquiv

source

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

source

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

source

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

source

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₂

source

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₂

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

⇑e '' s = ⇑e.symm ⁻¹' s

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

Equations

Instances For

source

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

source

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

source

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₃)

source

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

source

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

source

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

source

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

source

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

source

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.

Equations

Instances For

source

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

source

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

source

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.

Equations

Instances For

source

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

Documentation

Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv

Continuous affine equivalences #

Main definitions #

TODO #