affineIndependent_iff_not_collinear_set

English

Three points are affinely independent iff they are not collinear.

Русский

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

LaTeX

$$$\operatorname{AffineIndependent}_k(p_1,p_2,p_3) \iff \neg \operatorname{Collinear}_k(\{p_1,p_2,p_3\})$$$

Lean4

/-- Three points are affinely independent if and only if they are not collinear. -/
theorem affineIndependent_iff_not_collinear_set {p₁ p₂ p₃ : P} :
    AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k ({ p₁, p₂, p₃ } : Set P) :=
  by
  rw [affineIndependent_iff_not_collinear]
  simp_rw [Matrix.range_cons, Matrix.range_empty, Set.singleton_union, insert_empty_eq]

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