English
Let P be an affine space modeled on V over a ring R, and Q a torsor over W. Then the collection of continuous affine maps P →ᴬ[R] Q forms an affine space over the collection of continuous affine maps P →ᴬ[R] W.
Русский
Пусть P — аффинное пространство над V над кольцом R, и Q — торов над W. Тогда множество непрерывных аффинных отображений P →ᴬ[R] Q образует аффинное пространство над множеством непрерывных аффинных отображений P →ᴬ[R] W.
LaTeX
$$$\\text{ContAff}(P,Q) \\text{ is an affine space modeled on } \\text{ContAff}(P,W).$$$
Lean4
/-- The space of continuous affine maps from `P` to `Q` is an affine space over the space of
continuous affine maps from `P` to `W`. -/
instance : AddTorsor (P →ᴬ[R] W) (P →ᴬ[R] Q)
where
vadd f g := { __ := f.toAffineMap +ᵥ g.toAffineMap, cont := f.cont.vadd g.cont }
zero_vadd _ := ext fun _ ↦ zero_vadd _ _
add_vadd _ _ _ := ext fun _ ↦ add_vadd _ _ _
vsub f g := { __ := f.toAffineMap -ᵥ g.toAffineMap, cont := f.cont.vsub g.cont }
vsub_vadd' _ _ := ext fun _ ↦ vsub_vadd _ _
vadd_vsub' _ _ := ext fun _ ↦ vadd_vsub _ _
