English
For a finitely generated submodule p, spanRank(p) ≤ a iff there exists a generating set s with cardinality ≤ a and span R s = p.
Русский
Для конечнопорожденного p справедливо: spanRank(p) ≤ a тогда и только тогда, когда существует порождающее множество s такое, что |s| ≤ a и span R s = p.
LaTeX
$$$p.spanRank ≤ a \Leftrightarrow \exists s : Set M, \#s ≤ a ∧ span R s = p$$$
Lean4
/-- For a finitely generated submodule, its spanRank is less than or equal to a cardinal `a`
if and only if there is a generating subset with cardinality less than or equal to `a`. -/
theorem spanRank_le_iff_exists_span_set_card_le (p : Submodule R M) {a : Cardinal} :
p.spanRank ≤ a ↔ ∃ s : Set M, #s ≤ a ∧ span R s = p :=
by
constructor
· intro h
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p
exact ⟨s, ⟨hs₁ ▸ h, hs₂⟩⟩
· exact (fun ⟨s, ⟨hs₁, hs₂⟩⟩ ↦ hs₂.symm ▸ (le_trans (spanRank_span_le_card s) hs₁))
