affineIndependent_iff_not_collinear

English

A collinear set has a finite-dimensional vector span.

Русский

Коллинеарное множество имеет конечномерное векторное разложение.

LaTeX

$$$\operatorname{Collinear}_k(s) \Rightarrow \operatorname{FiniteDimensional}_k(\operatorname{vectorSpan}_k s)$$$

Lean4

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

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