Theorems · Theorem · combinatorics

Matroid.IsBasis.contract_eq_contract_delete

∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → M.contract X = (M.contract I).delete (X \ I)

Contracting a set is the same as contracting a basis for the set, and deleting the rest.

Defined in

Mathlib.Combinatorics.Matroid.Minor.Contract

Cited by

3 results in Mathlib

Foundations

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