English
For any X,Y ⊆ α and element e, inserting e into X ∩ Y and X ∪ Y preserves submodularity: eRk(insert e (X ∩ Y)) + eRk(insert e (X ∪ Y)) ≤ eRk(insert e X) + eRk(insert e Y).
Русский
Для любых X,Y ⊆ α и элемента e сохранится субмодулярность после добавления e в X ∩ Y и X ∪ Y: eRk(insert e (X ∩ Y)) + eRk(insert e (X ∪ Y)) ≤ eRk(insert e X) + eRk(insert e Y).
LaTeX
$$$M.eRk(\\operatorname{insert} e (X \\cap Y)) + M.eRk(\\operatorname{insert} e (X \\cup Y)) \\le M.eRk(\\operatorname{insert} e X) + M.eRk(\\operatorname{insert} e Y)$$$
Lean4
/-- A version of submodularity applied to the insertion of some `e` into two sets. -/
theorem eRk_insert_inter_add_eRk_insert_union_le (M : Matroid α) (X Y : Set α) :
M.eRk (insert e (X ∩ Y)) + M.eRk (insert e (X ∪ Y)) ≤ M.eRk (insert e X) + M.eRk (insert e Y) :=
by
rw [insert_inter_distrib, insert_union_distrib]
apply M.eRk_submod
