English
If every finite linearly independent subset of M has cardinality at most n, then the overall rank of M is at most n.
Русский
Если каждая конечная линейно независимая подмножество M имеет кардинал не более n, то общая размерность M не превосходит n.
LaTeX
$$$\left( \forall s \subseteq M, \text{Finite}, \operatorname{LinearIndependent} R\, s \Rightarrow |s| \le n \right) \Rightarrow \operatorname{rank}_R M \le n.$$$
Lean4
theorem rank_le {n : ℕ} (H : ∀ s : Finset M, (LinearIndependent R fun i : s => (i : M)) → s.card ≤ n) :
Module.rank R M ≤ n := by
rw [Module.rank_def]
apply ciSup_le'
rintro ⟨s, li⟩
exact linearIndependent_bounded_of_finset_linearIndependent_bounded H _ li
