Theorems · Theorem · combinatorics

Matroid.contract_delete_comm

∀ {α : Type u_1} {D C : Set α} (M : Matroid α), Disjoint C D → (M.contract C).delete D = (M.delete D).contract C

Contraction and deletion commute for disjoint sets.

Defined in

Mathlib.Combinatorics.Matroid.Minor.Contract

Cited by

3 results in Mathlib

Foundations

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