English
For any X,Y ⊆ α, the ENat-valued rank function is submodular: eRk(X ∩ Y) + eRk(X ∪ Y) ≤ eRk(X) + eRk(Y).
Русский
Для любых подмножеств X,Y ⊆ α функция ранга по ENat субмодулярна: eRk(X ∩ Y) + eRk(X ∪ Y) ≤ eRk(X) + eRk(Y).
LaTeX
$$$M.eRk(X \\cap Y) + M.eRk(X \\cup Y) \\le M.eRk(X) + M.eRk(Y)$$$
Lean4
/-- The `ℕ∞`-valued rank function is submodular. -/
theorem eRk_inter_add_eRk_union_le (M : Matroid α) (X Y : Set α) : M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk 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 [← hIX.eRk_eq_eRk_union, union_comm, ← hIY.eRk_eq_eRk_union, ← hIi.encard_eq_eRk, ← hIX.encard_eq_eRk, ←
hIY.encard_eq_eRk, union_comm, ← encard_union_add_encard_inter, add_comm]
exact add_le_add (eRk_le_encard _ _) (encard_mono (subset_inter hIX' hIY'))
