English
For any submodules p, q of M, the spanRank of their join satisfies: (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank.
Русский
Для любых подмодулей p, q модуля M выполняется: (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank.
LaTeX
$$$ (p \lor q).spanRank \le p\.spanRank + q\.spanRank. $$$
Lean4
theorem spanRank_sup_le_sum_spanRank {p q : Submodule R M} : (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank :=
by
apply (FG.spanRank_le_iff_exists_span_set_card_le (p ⊔ q)).mpr
obtain ⟨sp, ⟨hp₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank p
obtain ⟨sq, ⟨hq₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank q
exact ⟨sp ∪ sq, ⟨hp₁ ▸ hq₁ ▸ (Cardinal.mk_union_le sp sq), span_union sp sq⟩⟩