English
For an independent family p of submodules, the number of nontrivial members is bounded by the rank of M.
Русский
Для независимой семейства подпредметов число ненулевых членов ограничено рангом M.
LaTeX
$$$\forall p : ι \to \text{Submodule}_R M,\; \text{iSupIndep } p \Rightarrow \#\{i : p(i) \neq \bot\} \le \operatorname{rank}_R M$$$
Lean4
theorem subtype_ne_bot_le_rank [Nontrivial R] {V : ι → Submodule R M} (hV : iSupIndep V) :
Cardinal.lift.{v} #{ i : ι // V i ≠ ⊥ } ≤ Cardinal.lift.{w} (Module.rank R M) :=
by
set I := { i : ι // V i ≠ ⊥ }
have hI : ∀ i : I, ∃ v ∈ V i, v ≠ (0 : M) := by
intro i
rw [← Submodule.ne_bot_iff]
exact i.prop
choose v hvV hv using hI
have : LinearIndependent R v := (hV.comp Subtype.coe_injective).linearIndependent _ hvV hv
exact this.cardinal_lift_le_rank
