finiteDimensional_vectorSpan — Mathlib

English

If s is Coplanar, then vectorSpan_k s is finite dimensional.

Русский

Если s копланарно, то vectorSpan_k s конечномерно.

LaTeX

$$Coplanar(k,s) → FiniteDimensional_k(vectorSpan_k(s))$$

Lean4

/-- The `vectorSpan` of coplanar points is finite-dimensional. -/
theorem finiteDimensional_vectorSpan {s : Set P} (h : Coplanar k s) : FiniteDimensional k (vectorSpan k s) :=
  by
  refine IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 (lt_of_le_of_lt h ?_))
  exact Cardinal.lt_aleph0.2 ⟨2, rfl⟩

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