rank_add_le_rank_add_rank — Mathlib

English

For submodules s and t of M, the rank of s ⊔ t does not exceed the sum of ranks of s and t.

Русский

Для подмодулей s и t пространства M ранга объединения s ⊔ t не превышает суммы рангов s и t.

LaTeX

$$$\operatorname{rank}_R(s \vee t) \le \operatorname{rank}_R(s) + \operatorname{rank}_R(t).$$$

Lean4

theorem rank_add_le_rank_add_rank (s t : Submodule R M) :
    Module.rank R (s ⊔ t : Submodule R M) ≤ Module.rank R s + Module.rank R t :=
  by
  rw [← Submodule.rank_sup_add_rank_inf_eq]
  exact self_le_add_right _ _

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