span_eq_top_of_card_eq_finrank — Mathlib

English

Let V be a finite-dimensional K-vector space and b : ι → V be a linearly independent family with card ι = finrank K V. Then span K (range b) = ⊤.

Русский

Пусть V — конечномерное векторное пространство над K и b:ι → V — линейно независимая совокупность, удовлетворяющая |ι| = finrank_K V. Тогда span_K(range b) = ⊤.

LaTeX

$$$\\operatorname{span}_K(\\operatorname{range} b) = \\top$ при условии $\\operatorname{LinearIndependent}_K b$ и $\\operatorname{card}\\iota = \\operatorname{finrank}_K V$.$$

Lean4

theorem span_eq_top_of_card_eq_finrank {ι : Type*} [Nonempty ι] [Fintype ι] {b : ι → V}
    (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = finrank K V) : span K (Set.range b) = ⊤ :=
  have : FiniteDimensional K V := .of_finrank_pos <| card_eq ▸ Fintype.card_pos
  lin_ind.span_eq_top_of_card_eq_finrank' card_eq

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