English
cRk(X ∩ Y) + cRk(X ∪ Y) ≤ cRk(X) + cRk(Y).
Русский
Субмодулярность cRk: cRk(X ∩ Y) + cRk(X ∪ Y) ≤ cRk(X) + cRk(Y).
LaTeX
$$$cRk(X \cap Y) + cRk(X \cup Y) \le cRk(X) + cRk(Y)$$$
Lean4
/-- The `Cardinal` rank function is submodular. -/
theorem cRk_inter_add_cRk_union_le : M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y :=
by
obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)
obtain ⟨IX, hIX, hIX'⟩ := hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_left)
obtain ⟨IY, hIY, hIY'⟩ := hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_right)
rw [← cRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure, cRk_union_closure_eq, ←
hIi.cardinalMk_eq_cRk, ← hIX.cardinalMk_eq_cRk, ← hIY.cardinalMk_eq_cRk, ← mk_union_add_mk_inter, add_comm]
exact add_le_add (M.cRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))
