restrict_compl — Mathlib

English

Let M be a matroid with ground set E(M). For any subset D ⊆ E(M), the minor obtained by restricting M to the complement of D equals the minor obtained by deleting D; i.e., M|_{E(M) \\ D} = M \\ D.

Русский

Пусть M — матроид на базе E(M). Для любого подмножества D ⊆ E(M) минор, полученный ограничением M на дополнение D, совпадает с минором, полученным удалением D; то есть M|_{E(M) \\ D} = M \\ D.

LaTeX

$$$M\\restriction (M.E \\setminus D) = M \\setminus D$$$

Lean4

theorem restrict_compl (M : Matroid α) (D : Set α) : M ↾ (M.E \ D) = M ＼ D :=
  rfl

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