English
For a finite basis b and a finite spanning set w with span w = top, the index cardinality is bounded by w’s cardinality.
Русский
Для конечного базиса и конечного порождающего множества, если span w = top, то мощность индексов не превышает кардинал w.
LaTeX
$$$\text{span}(w) = \top \Rightarrow |ι| \le |w|$ (finite case).$$
Lean4
/-- Another auxiliary lemma for `Basis.le_span`, which does not require assuming the basis is finite,
but still assumes we have a finite spanning set.
-/
theorem basis_le_span' {ι : Type*} (b : Basis ι R M) {w : Set M} [Fintype w] (s : span R w = ⊤) : #ι ≤ Fintype.card w :=
by
haveI := nontrivial_of_invariantBasisNumber R
haveI := basis_finite_of_finite_spans w.toFinite s b
cases nonempty_fintype ι
rw [Cardinal.mk_fintype ι]
simp only [Nat.cast_le]
exact Basis.le_span'' b s
