Commit 2024-11-11 16:21 f7bf492f

View on Github →

feat(Data/Matroid/Closure): Spanning sets in matroids (#18129) We continue to build the API for matroid closure by defining a predicate Matroid.Spanning stating that a set X spans the ground set, or equivalently that X contains a base. We also state a couple of dozen API lemmas for this notion.

Estimated changes

Modified Mathlib/Data/Matroid/Closure.lean

added theorem Matroid.Base.spanning

added theorem Matroid.Base.spanning_of_superset

added theorem Matroid.Coindep.closure_compl

added theorem Matroid.Coindep.compl_spanning

added theorem Matroid.Indep.base_of_spanning

added theorem Matroid.Spanning.base_of_indep

added theorem Matroid.Spanning.closure_eq_of_superset

added theorem Matroid.Spanning.exists_base_subset

added theorem Matroid.Spanning.superset

added theorem Matroid.Spanning.union_left

added theorem Matroid.Spanning.union_right

added structure Matroid.Spanning

added theorem Matroid.closure_spanning_iff

added theorem Matroid.coindep_iff_closure_compl_eq_ground

added theorem Matroid.coindep_iff_compl_spanning

added theorem Matroid.ext_spanning

added theorem Matroid.ground_spanning

added theorem Matroid.not_spanning_iff_closure_ssubset

added theorem Matroid.spanning_iff_closure_eq

added theorem Matroid.spanning_iff_compl_coindep

added theorem Matroid.spanning_iff_exists_base_subset'

added theorem Matroid.spanning_iff_exists_base_subset

added theorem Matroid.spanning_iff_ground_subset_closure