lineMap_eq_left_iff — Mathlib

English

Equality with the left endpoint characterizes degenerate cases or zero parameter.

Русский

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

LaTeX

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

Lean4

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

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