English
Let s be an affine subspace of an affine space P with direction s. If a is a vector in the direction of s and b is a point of s, then translating b by a (via the affine action) coincides with adding a to b in the ambient vector space, i.e. the point obtained by the affine translation equals the vector sum of a (viewed as a vector) and b.
Русский
Пусть s — аффинное подпространство пространства P с направлением dir(s). Если a — вектор из направления s, а b — точка из s, то перенос b на a внутри аффинного пространства совпадает со суммированием a и b в соответствующем векторном пространстве: полученная точка равна a + b.
LaTeX
$$$\\\\uparrow\\\\left(a +\\\\!\\\\_v b\\\\right) = (a \\\\colon V) +\\\\!\\\\_v (b \\\\colon P) \\\\quad( s : AffineSubspace \\\\ k \\\\ P ), \\\\[Nonempty s], \\\\forall a \\\\in s.direction, \\\\forall b \\\\in s,$$$
Lean4
@[simp, norm_cast]
theorem coe_vadd (s : AffineSubspace k P) [Nonempty s] (a : s.direction) (b : s) : ↑(a +ᵥ b) = (a : V) +ᵥ (b : P) :=
rfl
