delete_isRestriction — Mathlib

English

For any matroid M and subset D ⊆ E(M), the minor M \\ D is a restriction of M to E(M) \\ D; equivalently, M \\ D ≤_r M.

Русский

Для любого матройда M и подмножества D ⊆ E(M) минора M \\ D является ограничением M на E(M) \\ D; эквивалентно M \\ D ≤_r M.

LaTeX

$$$(M\\setminus D)\\le_r M$$$

Lean4

@[simp]
theorem delete_isRestriction (M : Matroid α) (D : Set α) : M ＼ D ≤r M :=
  restrict_isRestriction _ _ diff_subset

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