Commit 2023-11-29 22:38 fb9a01ee

View on Github →

Matroid independence axioms (#8071) This PR provides several ways to construct a matroid with alternative versions of the axiom sets, in particular in terms of an independence predicate. It will be used to define duals and minors of matroids in future PRs.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Matroid/Basic.lean

added theorem Matroid.Base.mem_of_insert_indep

added theorem Matroid.Basis'.insert_not_indep

added theorem Matroid.Indep.exists_insert_of_not_mem_maximals

deleted theorem Matroid.exists_base

Created Mathlib/Data/Matroid/IndepAxioms.lean

added theorem IndepMatroid.matroid_indep_iff

added theorem IndepMatroid.ofBddAugment_E

added theorem IndepMatroid.ofBddAugment_indep

added theorem IndepMatroid.ofBdd_indep

added theorem IndepMatroid.ofFinitary_indep

added theorem IndepMatroid.ofFinite_E

added theorem IndepMatroid.ofFinite_indep

added theorem IndepMatroid.ofFinset_E

added theorem IndepMatroid.ofFinset_indep'

added theorem IndepMatroid.ofFinset_indep

added structure IndepMatroid

added theorem Matroid.existsMaximalSubsetProperty_of_bdd

added theorem Matroid.ofBaseOfFinite_E

added theorem Matroid.ofBaseOfFinite_base

added theorem Matroid.ofExistsFiniteBase_base