delete_closure_eq — Mathlib

English

The closure in the minor equals the closure in the original restricted to X minus D, with D removed.

Русский

Замыкание в производном равняется замыканию в исходном, ограниченному на X \ D, затем удаляем D.

LaTeX

$$$ (M \setminus D).closure(X) = M.closure(X \setminus D) \setminus D $$$

Lean4

@[simp]
theorem delete_closure_eq (M : Matroid α) (D X : Set α) : (M ＼ D).closure X = M.closure (X \ D) \ D :=
  by
  rw [← restrict_compl, restrict_closure_eq', sdiff_sdiff_self, bot_eq_empty, union_empty, diff_eq, inter_comm M.E, ←
    inter_assoc X, ← diff_eq, closure_inter_ground, ← inter_assoc, ← diff_eq, inter_eq_left]
  exact diff_subset.trans (M.closure_subset_ground _)

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