collinear_iff_not_affineIndependent_of_ne

English

If three indices i1,i2,i3 are pairwise distinct, then Collinear holds iff the corresponding triple is not affine independent.

Русский

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

LaTeX

$$$\operatorname{Collinear}_k(\{ p_{i1}, p_{i2}, p_{i3} \}) \iff \neg \operatorname{AffineIndependent}_k( p )$$$

Lean4

/-- Three points are collinear if and only if they are not affinely independent. -/
theorem collinear_iff_not_affineIndependent_of_ne {p : Fin 3 → P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃)
    (h₂₃ : i₂ ≠ i₃) : Collinear k ({p i₁, p i₂, p i₃} : Set P) ↔ ¬AffineIndependent k p :=
  (affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃).not_left.symm

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