Commit 2023-10-30 21:12 aaa97c71

View on Github →

feat: (Data.Matroid) basic matroid theory (#6352) This PR is the first in a series that are intended to add matroid theory to mathlib. The file Data.Matroid.Basic contains the definition of (possibly infinite) matroids, API relating bases, independent/dependent sets and bases of sets, and some simple typeclasses related to finiteness/nonemptiness of matroids. We also define a tactic whose job is to prove that a set is contained in the ground set of a matroid (using aesop); it is imperfect, but does an ok job.

Alternative axiomatizations, duality, minors, rank, circuits, closure, flats, etc etc are all ready to go, and will be added in a sequence of future PRs.

Estimated changes

added theorem Matroid.Base.exchange
added theorem Matroid.Base.finite
added theorem Matroid.Base.indep
added theorem Matroid.Base.infinite
added theorem Matroid.Base.nonempty
added theorem Matroid.Basis'.basis
added theorem Matroid.Basis'.indep
added theorem Matroid.Basis'.subset
added def Matroid.Basis'
added theorem Matroid.Basis.Finite
added theorem Matroid.Basis.basis'
added theorem Matroid.Basis.indep
added theorem Matroid.Basis.subset
added def Matroid.Basis
added theorem Matroid.Dep.nonempty
added theorem Matroid.Dep.not_indep
added theorem Matroid.Dep.superset
added def Matroid.Dep
added theorem Matroid.Indep.diff
added theorem Matroid.Indep.finite
added theorem Matroid.Indep.not_dep
added theorem Matroid.Indep.subset
added def Matroid.Indep
added theorem Matroid.basis_iff'
added theorem Matroid.basis_iff
added theorem Matroid.dep_iff
added theorem Matroid.empty_indep
added theorem Matroid.empty_not_base
added theorem Matroid.exists_base
added theorem Matroid.exists_basis'
added theorem Matroid.exists_basis
added theorem Matroid.ground_finite
added theorem Matroid.indep_or_dep
added theorem Matroid.not_dep_iff
added theorem Matroid.not_finiteRk
added theorem Matroid.not_indep_iff
added theorem Matroid.not_infiniteRk
added theorem Matroid.setOf_basis_eq
added theorem Matroid.setOf_dep_eq
added theorem Matroid.setOf_indep_eq
added theorem Matroid.set_finite
added structure Matroid