eRk_compl_union_add_eRk_compl_inter_le

English

For X,Y ⊆ ground set E, the ENat-valued rank is submodular on complements: eRk(E \\ (X ∪ Y)) + eRk(E \\ (X ∩ Y)) ≤ eRk(E \\ X) + eRk(E \\ Y).

Русский

Для подмножеств X,Y множества E применима субмодулярность к дополнениям: eRk(E \ (X ∪ Y)) + eRk(E \ (X ∩ Y)) ≤ eRk(E \ X) + eRk(E \ Y).

LaTeX

$$$M.eRk (M.E \\ (X \\cup Y)) + M.eRk (M.E \\ (X \\cap Y)) \\le M.eRk (M.E \\ X) + M.eRk (M.E \\ Y)$$$

Lean4

/-- A version of submodularity applied to the complements of two sets. -/
theorem eRk_compl_union_add_eRk_compl_inter_le (M : Matroid α) (X Y : Set α) :
    M.eRk (M.E \ (X ∪ Y)) + M.eRk (M.E \ (X ∩ Y)) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y) :=
  by
  rw [← diff_inter_diff, diff_inter]
  apply M.eRk_submod

Похожие утверждения