delete — Mathlib

English

A variant expressing a general form of the interaction between delete and contract without disjointness constraints.

Русский

Обобщенная форма взаимодействия удаления и сжатия без ограничений на непересечение.

LaTeX

$$(M.delete D).contract C = M.contract (C \ D) .delete D$$

Lean4

/-- The deletion `M ＼ D` is the restriction of a matroid `M` to `M.E \ D`.
Its independent sets are the `M`-independent subsets of `M.E \ D`. -/
def delete (M : Matroid α) (D : Set α) : Matroid α :=
  M ↾ (M.E \ D)

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