lineMap_apply_one_sub — Mathlib

English

The parameterized line remains consistent under swapping and reparameterization.

Русский

Параметризация прямой сохраняется при перестановке и повторном параметрировании.

LaTeX

$$$ lineMap(p_0,p_1)(1-c) = lineMap(p_1,p_0)(c) $$$

Lean4

@[simp]
theorem lineMap_apply_one_sub (p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ (1 - c) = lineMap p₁ p₀ c :=
  by
  rw [lineMap_symm p₀, comp_apply]
  congr
  simp [lineMap_apply]

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