lineMap_eq_right_iff — Mathlib

English

Equality with the right endpoint characterizes degenerate cases or unit parameter.

Русский

Эквивалентность правой точки характеризует вырожденные случаи или единичный параметр.

LaTeX

$$$ lineMap(p_0,p_1)(c) = p_1 \iff p_0 = p_1 \lor c = 1 $$$

Lean4

@[simp]
theorem lineMap_eq_right_iff [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c : k} : lineMap p₀ p₁ c = p₁ ↔ p₀ = p₁ ∨ c = 1 :=
  by rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_one]

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