English
If b is a basis and v is a linearly independent family, then |κ| ≤ |ι|, where ι is the index set of the basis.
Русский
Если b базис и v линейно независимы, то |κ| ≤ |ι| для индексов базиса.
LaTeX
$$$\text{If } b:\ Basis_ι R M, \ v:\kappa \to M \text{ LI}, \ |\kappa| \le |\iota|.$$$
Lean4
/-- Over any ring `R` satisfying the strong rank condition,
if `b` is a basis for a module `M`,
and `s` is a linearly independent set,
then the cardinality of `s` is bounded by the cardinality of `b`.
-/
theorem linearIndependent_le_basis {ι : Type w} (b : Basis ι R M) {κ : Type w} (v : κ → M) (i : LinearIndependent R v) :
#κ ≤ #ι := by
classical
-- We split into cases depending on whether `ι` is infinite.
cases fintypeOrInfinite ι
· rw [Cardinal.mk_fintype ι] -- When `ι` is finite, we have `linearIndependent_le_span`,
haveI : Nontrivial R := nontrivial_of_invariantBasisNumber R
rw [Fintype.card_congr (Equiv.ofInjective b b.injective)]
exact linearIndependent_le_span v i (range b) b.span_eq
· -- and otherwise we have `linearIndependent_le_infinite_basis`.
exact linearIndependent_le_infinite_basis b v i
