English
For X,Y ⊆ α and e, the submodularity statement holds for the complements after inserting e: eRk(M.E \\ insert e (X ∪ Y)) + eRk(M.E \\ insert e (X ∩ Y)) ≤ eRk(M.E \\ insert e X) + eRk(M.E \\ insert e Y).
Русский
Для X,Y ⊆ α и e справедлива субмодулярность для дополнений после вставки: eRk(M.E \\ insert e (X ∪ Y)) + eRk(M.E \\ insert e (X ∩ Y)) ≤ eRk(M.E \\ insert e X) + eRk(M.E \\ insert e Y).
LaTeX
$$$M.eRk (M.E \\ insert e (X \\cup Y)) + M.eRk (M.E \\ insert e (X \\cap Y)) \\le M.eRk (M.E \\ insert e X) + M.eRk (M.E \\ insert e Y)$$$
Lean4
/-- A version of submodularity applied to the complements of two insertions. -/
theorem eRk_compl_insert_union_add_eRk_compl_insert_inter_le (M : Matroid α) (X Y : Set α) :
M.eRk (M.E \ insert e (X ∪ Y)) + M.eRk (M.E \ insert e (X ∩ Y)) ≤
M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y) :=
by
rw [insert_union_distrib, insert_inter_distrib]
exact M.eRk_compl_union_add_eRk_compl_inter_le (insert e X) (insert e Y)
