lineMap_lineMap_left — Mathlib

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]

Похожие утверждения