English
The fundamental circuit of e and I is the unique circuit contained in insert e I under appropriate independence assumptions.
Русский
Фундаментальный цикл элемента e и множества I — уникальный цикл внутри вставки e в I при подходящих условиях независимости.
LaTeX
$$$M.IsCircuit (\text{insert } e \ I)$ under the usual conditions; more precisely, the construction defines a circuit contained in insert e I.$$
Lean4
/-- 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`. -/
def fundCircuit (M : Matroid α) (e : α) (I : Set α) : Set α :=
insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure { e } ⊆ M.closure J})
