collinear_iff_not_affineIndependent

English

Three points are collinear if and only if they are not affinely independent.

Русский

Три точки коллинеарны тогда и только тогда, когда они аффинно зависимы.

LaTeX

$$$\text{Three points are collinear} \iff \neg \operatorname{AffineIndependent}_k(p_1,p_2,p_3)$$$

Lean4

/-- Three points are collinear if and only if they are not affinely
independent. -/
theorem collinear_iff_not_affineIndependent {p : Fin 3 → P} : Collinear k (Set.range p) ↔ ¬AffineIndependent k p := by
  rw [collinear_iff_finrank_le_one, finrank_vectorSpan_le_iff_not_affineIndependent k p (Fintype.card_fin 3)]

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