collinear_iff_not_affineIndependent_set

English

Three points are affinely independent if and only if they are not collinear, provided their indices are distinct.

Русский

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

LaTeX

$$$\text{Three points are affinely independent iff not Collinear}$ with non-equality of indices; formal content is: $\operatorname{affineIndependent}_k(p) \iff \neg \operatorname{Collinear}_k(\{p_{i_1}, p_{i_2}, p_{i_3}\})$ for distinct indices.$$

Lean4

/-- Three points are collinear if and only if they are not affinely independent. -/
theorem collinear_iff_not_affineIndependent_set {p₁ p₂ p₃ : P} :
    Collinear k ({ p₁, p₂, p₃ } : Set P) ↔ ¬AffineIndependent k ![p₁, p₂, p₃] :=
  affineIndependent_iff_not_collinear_set.not_left.symm

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