English
If a basis is infinite, then any linearly independent family contained in the span of that basis is bounded in size by the basis.
Русский
Если база бесконечна, любая линейно независимая семейство, лежащая в области порожденной базой, ограничено по размеру.
LaTeX
$$$\text{If } b \text{ is infinite, and } v \text{ is LI with } \operatorname{span} v \subseteq \operatorname{span} b, \ |\kappa| \le |\iota|.$$$
Lean4
/-- If `R` satisfies the rank condition,
then the cardinality of any basis is bounded by the cardinality of any spanning set.
-/
theorem le_span {J : Set M} (v : Basis ι R M) (hJ : span R J = ⊤) : #(range v) ≤ #J :=
by
haveI := nontrivial_of_invariantBasisNumber R
cases fintypeOrInfinite J
· rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]
convert Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)
simp
· let S : J → Set ι := fun j => ↑(v.repr j).support
let S' : J → Set M := fun j => v '' S j
have hs : range v ⊆ ⋃ j, S' j := by
intro b hb
rcases mem_range.1 hb with ⟨i, hi⟩
have : span R J ≤ comap v.repr.toLinearMap (Finsupp.supported R R (⋃ j, S j)) :=
span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
rw [hJ] at this
replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single_ne_zero _ one_ne_zero] at this
· subst b
rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩
refine le_of_not_gt fun IJ => ?_
suffices #(⋃ j, S' j) < #(range v) by exact not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩
refine lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_
· exact fun j => (Cardinal.lt_aleph0_of_finite _).le
· simpa
