Theorems · Definition · combinatorics

Matroid.ofExistsMatroid

{α : Type u_1} → (E : Set α) → (Indep : Set α → Prop) → (∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I) → Matroid α

Construct an Matroid from an independence predicate that agrees with that of some matroid M. This is computable even if M is only known existentially, or when M exists for different reasons in different cases. This can also be used to change the independence predicate to a more useful definitional form.

Defined in

Mathlib.Combinatorics.Matroid.IndepAxioms

Cited by

1 results in Mathlib

Foundations

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