finiteDimensional_vectorSpan — Mathlib

English

A collinear set has a finite-dimensional vector span.

Русский

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

LaTeX

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

Lean4

/-- The `vectorSpan` of collinear points is finite-dimensional. -/
theorem finiteDimensional_vectorSpan {s : Set P} (h : Collinear k s) : FiniteDimensional k (vectorSpan k s) :=
  IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 (lt_of_le_of_lt h Cardinal.one_lt_aleph0))

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