Theorems · Theorem · combinatorics

Matroid.contract_spanning_iff

∀ {α : Type u_1} {M : Matroid α} {X C : Set α},
  autoParam (C ⊆ M.E) Matroid.contract_spanning_iff._auto_1 →
    ((M.contract C).Spanning X ↔ M.Spanning (X ∪ C) ∧ Disjoint X C)

Defined in: Mathlib.Combinatorics.Matroid.Minor.Contract
Cited by: 1 results in Mathlib
Foundations: Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Disjointstatement and proof · cited by 2,201
Matroidstatement and proof · cited by 1,258
Matroid.Estatement and proof · cited by 550
Matroid.closureproof · cited by 272
Set.subset_union_rightproof · cited by 123
Matroid.contractstatement and proof · cited by 103
Matroid.Spanningstatement and proof · cited by 63
Set.subset_sdiffproof · cited by 29
Set.union_subset_iffproof · cited by 21
Set.union_sdiff_cancelproof · cited by 16
Matroid.contract_groundproof · cited by 12

Cited by1

Results whose statement or proof uses this declaration.

Matroid.contract_spanning_iff'proof · cited by 1