delete_subset_ground — Mathlib

English

For any matroid M and D ⊆ E(M), the ground of the deletion is contained in the ground of M: (M \\ D).E ⊆ M.E.

Русский

Для любого матроидa M и D ⊆ E(M) основание удаления содержится в основание M: (M \\ D).E ⊆ M.E.

LaTeX

$$$(M\\setminus D).E \\subseteq M.E$$$

Lean4

@[aesop unsafe 10% (rule_sets := [Matroid])]
theorem delete_subset_ground (M : Matroid α) (D : Set α) : (M ＼ D).E ⊆ M.E :=
  diff_subset

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