Theorems · Theorem · combinatorics

Matroid.contract_closure_eq_contract_delete

∀ {α : Type u_1} (M : Matroid α) (C : Set α), M.contract (M.closure C) = (M.contract C).delete (M.closure C \ C)

Contracting the closure of a set is the same as contracting the set, and then deleting the rest of its elements.

Defined in

Mathlib.Combinatorics.Matroid.Minor.Contract

Cited by

0 results in Mathlib

Foundations

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