English
The line map is the affine map that parameterizes the line from p0 to p1, sending 0 to p0 and 1 to p1, with intermediate values given by p0 plus a scaled direction towards p1.
Русский
Line map представляет собой аффинное отображение, задающее прямую от p0 к p1: 0 достигает p0, 1 достигает p1, а промежуточные значения задаются умножением направления на скаляр.
LaTeX
$$$\text{lineMap}(p_0,p_1) : k \to^\mathrm{aff} P_1$ равно карте, которая отправляет $t$ в $t\cdot(p_1-p_0)+p_0$ (векторная вычитание вектор-сложение в аффинном контексте).$$
Lean4
/-- The affine map from `k` to `P1` sending `0` to `p₀` and `1` to `p₁`. -/
def lineMap (p₀ p₁ : P1) : k →ᵃ[k] P1 :=
((LinearMap.id : k →ₗ[k] k).smulRight (p₁ -ᵥ p₀)).toAffineMap +ᵥ const k k p₀
