Theorems · Definition · combinatorics

Matroid.fundCircuit

{α : Type u_1} → Matroid α → α → Set α → Set α

For an independent set I and some e ∈ M.closure I \ I, M.fundCircuit e I is the unique circuit contained in insert e I. For the fact that this is a circuit, see Matroid.Indep.fundCircuit_isCircuit, and the fact that it is unique, see Matroid.IsCircuit.eq_fundCircuit_of_subset. Has the junk value {e} if e ∈ I or e ∉ M.E, and insert e I if e ∈ M.E \ M.closure I.

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

19 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms