English
For an independent family p, an auxiliary bound holds: cardinal of nonzero submodules ≤ finrank M.
Русский
Для независимой семейства p выполняется вспомогательное неравенство: число ненулевых подпредметов не превосходит finrank M.
LaTeX
$$$\forall p : ι \to \text{Submodule}_R M,\; \text{iSupIndep } p \Rightarrow \operatorname{Cardinal}.lift(\#\{ i : p(i) \neq \bot \}) \le (\operatorname{finrank} R M).cast$$$
Lean4
/-- If `p` is an independent family of submodules of a `R`-finite module `M`, then the
number of nontrivial subspaces in the family `p` is bounded above by the dimension of `M`.
Note that the `Fintype` hypothesis required here can be provided by
`iSupIndep.fintypeNeBotOfFiniteDimensional`. -/
theorem subtype_ne_bot_le_finrank {p : ι → Submodule R M} (hp : iSupIndep p) [Fintype { i // p i ≠ ⊥ }] :
Fintype.card { i // p i ≠ ⊥ } ≤ finrank R M := by simpa using hp.subtype_ne_bot_le_finrank_aux
