English
For submodules s and t of M, the sum of the ranks of s ⊔ t and s ∩ t equals the sum of the ranks of s and t.
Русский
Для подмодулей s и t пространства M верно: сумма рангов s ⊔ t и s ∩ t равна сумме рангов s и t.
LaTeX
$$$\operatorname{rank}_R(s \vee t) + \operatorname{rank}_R(s \wedge t) = \operatorname{rank}_R(s) + \operatorname{rank}_R(t).$$$
Lean4
theorem rank_sup_add_rank_inf_eq (s t : Submodule R M) :
Module.rank R (s ⊔ t : Submodule R M) + Module.rank R (s ⊓ t : Submodule R M) = Module.rank R s + Module.rank R t :=
by
conv_rhs => enter [2]; rw [show t = (s ⊔ t) ⊓ t by simp]
rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype), ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype), comap_inf,
(quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf, (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq,
Submodule.map_comap_subtype, (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype, ←
inf_assoc, inf_idem, add_right_comm]
