Theorems · Theorem · combinatorics

Matroid.fundCircuit_eq_of_mem

∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α}, e ∈ X → M.fundCircuit e X = {e}

The fundamental isCircuit of e and X has the junk value {e} if e ∈ X

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

2 results in Mathlib

Foundations

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