Theorems · Definition · combinatorics

Matroid.delete

{α : Type u_1} → Matroid α → Set α → Matroid α

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.

Defined in

Mathlib.Combinatorics.Matroid.Minor.Delete

Cited by

86 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound