ofSpan — Mathlib

English

If a subset s spans the space, then there exists a basis of V contained in s.

Русский

Если множество s порождает все пространство, то существует базис V, состоящий из элементов s.

LaTeX

$$$\\exists B\\subseteq s\\text{ such that } B\\text{ is a basis of } V$$$

Lean4

/-- If a set `s` spans the space, this is a basis contained in `s`. -/
noncomputable def ofSpan (hs : ⊤ ≤ span K s) : Basis ((linearIndepOn_empty K id).extend (empty_subset s)) K V :=
  extendLe (linearIndependent_empty K V) (empty_subset s) hs

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