English
Let P be an affine space modeled on a vector space V over a ring k, with a topology. For every v in V, the map p ↦ v +ᵥ p is a continuous affine automorphism of P.
Русский
Пусть P — аффинное пространство над векторным пространством V над кольцом k, с топологией. Для каждого v ∈ V отображение p ↦ v +ᵥ p является непрерывным аффинным автопреобразованием пространства P.
LaTeX
$$$\forall v \in V_1,\; \exists \phi_v \in Aut_{\mathrm{Aff}}(P_1)\text{ such that } \phi_v(p) = v +\!_{p} p \text{ for all } p \in P_1.$$$
Lean4
/-- The map `p ↦ v +ᵥ p` as a continuous affine automorphism of an affine space
on which addition is continuous. -/
def constVAdd [ContinuousConstVAdd V₁ P₁] (v : V₁) : P₁ ≃ᴬ[k] P₁
where
toAffineEquiv := AffineEquiv.constVAdd k P₁ v
continuous_toFun := continuous_const_vadd v
continuous_invFun := continuous_const_vadd (-v)
