English
Let V be a finite-dimensional K-vector space and b : ι → V be a linearly independent family indexed by a finite set ι. If the cardinality of ι equals the dimension of V, then the span of the range of b is the whole space V.
Русский
Пусть V — конечномерное пространство над K, и b: ι → V — линейно независимая совокупность, индексированная конечным множеством ι. Если кардинал ι равен размерности V, тоspan(диапазон b) = V.
LaTeX
$$$\\operatorname{span}_K(\\operatorname{range} b) = \\top$ при условии $\\operatorname{LinearIndependent}_K b$ и $|\\iota| = \\operatorname{finrank}_K V$.$$
Lean4
theorem span_eq_top_of_card_eq_finrank' {ι : Type*} [Fintype ι] [FiniteDimensional K V] {b : ι → V}
(lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = finrank K V) : span K (Set.range b) = ⊤ :=
by
by_contra ne_top
rw [← finrank_span_eq_card lin_ind] at card_eq
exact ne_of_lt (Submodule.finrank_lt ne_top) card_eq
