English
If hs and ht hold for subsets with quotient, then the union has rank as the sum of ranks.
Русский
Если выполняются условия для hs и ht по множествам с фактором, то объединение имеет ранг как сумма рангов.
LaTeX
$$$\text{rank}(s \cup t) = \text{rank}(s) + \text{rank}(t)$$$
Lean4
theorem rank_quotient_add_rank_le [Nontrivial R] (M' : Submodule R M) :
Module.rank R (M ⧸ M') + Module.rank R M' ≤ Module.rank R M :=
by
conv_lhs => simp only [Module.rank_def]
rw [Cardinal.ciSup_add_ciSup _ (bddAbove_range _) _ (bddAbove_range _)]
refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_
choose f hf using Submodule.Quotient.mk_surjective M'
simpa [add_comm] using
(LinearIndependent.sumElim_of_quotient ht (fun (i : s) ↦ f i)
(by simpa [Function.comp_def, hf] using hs)).cardinal_le_rank
