lineMap_eq_lineMap_iff — Mathlib

English

The parameter substitution 1 - c reverses the order of the endpoints.

Русский

Замена 1 - c обращает направления прямой.

LaTeX

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

Lean4

@[simp]
theorem lineMap_eq_lineMap_iff [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c₁ c₂ : k} :
    lineMap p₀ p₁ c₁ = lineMap p₀ p₁ c₂ ↔ p₀ = p₁ ∨ c₁ = c₂ := by
  rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ← sub_smul, smul_eq_zero,
    sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]

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