eRk_compl_union_of_disjoint — Mathlib

English

Let X and Y be subsets of the ground with X and Y disjoint. Then the eRk of (E \ X) ∪ Y does not depend on Y; in fact M.eRk((E \\ X) ∪ Y) = M.eRk(E \\ X).

Русский

Пусть X, Y подмножества опорного множества E матроида, причём X и Y непересекаются. Тогда eRk((E \ X) ∪ Y) не зависит от Y и равен eRk(E \ X).

LaTeX

$$$ X \\cap Y = \\varnothing \\Rightarrow M.eRk((M.E \\setminus X) \\cup Y) = M.eRk(M.E \\setminus X) $$$

Lean4

theorem eRk_compl_union_of_disjoint (M : Matroid α) (hXY : Disjoint X Y) : M.eRk (M.E \ X ∪ Y) = M.eRk (M.E \ X) := by
  rw [← eRk_inter_ground, union_inter_distrib_right, inter_eq_self_of_subset_left diff_subset,
    union_eq_self_of_subset_right (subset_diff.2 ⟨inter_subset_right, hXY.symm.mono_left inter_subset_left⟩)]

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