Theorems · Definition · combinatorics

Matroid.closure

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

The closure of X ⊆ M.E is the intersection of all the flats of M containing X. A set X that doesn't satisfy X ⊆ M.E has the junk value M.closure X := M.closure (X ∩ M.E).

Defined in

Mathlib.Combinatorics.Matroid.Closure

Cited by

272 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 24 definitions · uses no axioms