English
If J spans M, then the cardinality of the basis index set is bounded by the cardinality of J.
Русский
Если J порождает M, то размер индексов базиса не превосходит кардинала J.
LaTeX
$$$\operatorname{span}_R J = \top \Rightarrow |ι| \le |J|$.$$
Lean4
/-- An auxiliary lemma for `Basis.le_span`.
If `R` satisfies the rank condition,
then for any finite basis `b : Basis ι R M`,
and any finite spanning set `w : Set M`,
the cardinality of `ι` is bounded by the cardinality of `w`.
-/
theorem le_span'' {ι : Type*} [Fintype ι] (b : Basis ι R M) {w : Set M} [Fintype w] (s : span R w = ⊤) :
Fintype.card ι ≤ Fintype.card w := by
-- We construct a surjective linear map `(w → R) →ₗ[R] (ι → R)`,
-- by expressing a linear combination in `w` as a linear combination in `ι`.
fapply card_le_of_surjective' R
· exact b.repr.toLinearMap.comp (Finsupp.linearCombination R (↑))
· apply Surjective.comp (g := b.repr.toLinearMap)
· apply LinearEquiv.surjective
rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination]
simpa using s
