Theorems · Theorem · combinatorics

Matroid.fundCocircuit_eq_of_notMem_ground

∀ {α : Type u_1} {M : Matroid α} {e : α} (X : Set α), e ∉ M.E → M.fundCocircuit e X = {e}

The fundamental cocircuit of X and e has the junk value {e} if e ∉ M.E

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

1 results in Mathlib

Foundations

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