spanRank_sup_le_sum_spanRank — Mathlib

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⟩⟩

Похожие утверждения