English
LineMap composed on the left yields a new line with parameter 1 − (1 − d)(1 − c): lineMap(lineMap(p0,p1,c), p1, d) = lineMap(p0,p1, 1 − (1 − d)(1 − c)).
Русский
Левая композиция LineMap даёт новую прямую с параметром 1 − (1 − d)(1 − c): lineMap(lineMap(p0,p1,c), p1, d) = lineMap(p0,p1,1 − (1 − d)(1 − c)).
LaTeX
$$$ lineMap(lineMap(p_0,p_1,c), p_1, d) = lineMap(p_0,p_1, 1 - (1 - d) \\cdot (1 - c)) $$$
Lean4
@[simp]
theorem lineMap_lineMap_left (p₀ p₁ : P1) (c d : k) :
lineMap (lineMap p₀ p₁ c) p₁ d = lineMap p₀ p₁ (1 - (1 - d) * (1 - c)) := by
simp_rw [lineMap_apply_one_sub, ← lineMap_apply_one_sub p₁, lineMap_lineMap_right]