Theorems · Theorem · combinatorics

Matroid.IsCircuit.eq_fundCircuit_of_subset

∀ {α : Type u_1} {M : Matroid α} {C I : Set α} {e : α},
  M.IsCircuit C → M.Indep I → C ⊆ insert e I → C = M.fundCircuit e I

For I independent, M.fundCircuit e I is the only circuit contained in insert e I.

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

0 results in Mathlib

Foundations

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