Theorems · Inductive type · combinatorics

Matroid

Type u_1 → Type u_1

A Matroid α is a ground set E of type Set α, and a nonempty collection of its subsets satisfying the exchange property and the maximal subset property. Each such set is called a Base of M. An Independent set is just a set contained in a base, but we include this predicate as a structure field for better definitional properties. In most cases, using this definition directly is not the best way to construct a matroid, since it requires specifying both the bases and independent sets. If the bases are known, use Matroid.ofBase or a variant. If just the independent sets are known, define an IndepMatroid, and then use IndepMatroid.matroid.

Defined in

Mathlib.Combinatorics.Matroid.Basic

Cited by

1,258 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms