collinear_singleton — Mathlib

English

If a set is collinear, its vector span is finite-dimensional.

Русский

Если множество коллинеарно, то его векторное пространство порождения конечно по размерности.

LaTeX

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

Lean4

/-- A single point is collinear. -/
theorem collinear_singleton (p : P) : Collinear k ({ p } : Set P) :=
  by
  rw [collinear_iff_rank_le_one, vectorSpan_singleton]
  simp

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