affineIndependent_iff_not_collinear_of_ne

English

Three points are affinely independent iff they are not collinear, with ne conditions on indices.

Русский

Три точки равнозначно аффинно независимы и не коллинеарны с условиями на индексы.

LaTeX

$$$\operatorname{AffineIndependent}_k(p) \iff \neg \operatorname{Collinear}_k(\{p_{i_1}, p_{i_2}, p_{i_3}\})$$$

Lean4

/-- Three points are affinely independent if and only if they are not collinear. -/
theorem affineIndependent_iff_not_collinear_of_ne {p : Fin 3 → P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃)
    (h₂₃ : i₂ ≠ i₃) : AffineIndependent k p ↔ ¬Collinear k ({p i₁, p i₂, p i₃} : Set P) :=
  by
  have hu : (Finset.univ : Finset (Fin 3)) = { i₁, i₂, i₃ } := by decide +revert
  rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu, Finset.coe_insert,
    Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]

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