English
For an independent family p, the number of nontrivial submodules is bounded by finrank R M.
Русский
Для независимой семейства p число ненулевых подпредметов ограничено finrank R M.
LaTeX
$$$\forall p : ι \to \text{Submodule}_R M,\; \text{iSupIndep } p \Rightarrow \#\{i : p(i) \neq \bot\} \le \operatorname{finrank}_R(M)$$$
Lean4
theorem subtype_ne_bot_le_finrank_aux {p : ι → Submodule R M} (hp : iSupIndep p) :
#{ i // p i ≠ ⊥ } ≤ (finrank R M : Cardinal.{w}) :=
by
suffices Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{v} (finrank R M : Cardinal.{w}) by
rwa [Cardinal.lift_le] at this
calc
Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{w} (Module.rank R M) := hp.subtype_ne_bot_le_rank
_ = Cardinal.lift.{w} (finrank R M : Cardinal.{v}) := by rw [finrank_eq_rank]
_ = Cardinal.lift.{v} (finrank R M : Cardinal.{w}) := by simp
