English
If ι is infinite, then for maximal LI v, the inequality |ι| ≤ |κ| holds (up to lifting).
Русский
Если индексный набор бесконечен, то для максимальной линейно независимой последовательности выполняется неравенство |ι| ≤ |κ|.
LaTeX
$$$\\#ι \\le \\#κ$ (up to lifting)$$
Lean4
/-- Over any ring `R`, if `b` is an infinite basis for a module `M`,
and `s` is a maximal linearly independent set,
then the cardinality of `b` is bounded by the cardinality of `s`.
-/
theorem infinite_basis_le_maximal_linearIndependent' {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w'}
(v : κ → M) (i : LinearIndependent R v) (m : i.Maximal) : Cardinal.lift.{w'} #ι ≤ Cardinal.lift.{w} #κ :=
by
let Φ := fun k : κ => (b.repr (v k)).support
have w₁ : #ι ≤ #(Set.range Φ) := by
apply Cardinal.le_range_of_union_finset_eq_top
exact union_support_maximal_linearIndependent_eq_range_basis b v i m
have w₂ : Cardinal.lift.{w'} #(Set.range Φ) ≤ Cardinal.lift.{w} #κ := Cardinal.mk_range_le_lift
exact (Cardinal.lift_le.mpr w₁).trans w₂
