lineMap_lineMap_right — Mathlib

English

LineMap composed with another lineMap yields a single line along the same base that scales by the product of parameters: lineMap(p0, lineMap(p0, p1, c), d) = lineMap(p0, p1, d c).

Русский

Линейная карта, применённая к результирующей точке второй карты, даёт линию с параметром, равным произведению параметров: lineMap(p0, lineMap(p0,p1,c), d) = lineMap(p0,p1, d c).

LaTeX

$$$ lineMap(p_0, lineMap(p_0,p_1,c), d) = lineMap(p_0,p_1, d \\cdot c) $$$

Lean4

@[simp]
theorem lineMap_lineMap_right (p₀ p₁ : P1) (c d : k) : lineMap p₀ (lineMap p₀ p₁ c) d = lineMap p₀ p₁ (d * c) := by
  simp [lineMap_apply, mul_smul]

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