Commit 2025-01-25 17:33 ae9766f5

View on Github →

feat(Data/Matroid/Closure): matroid closure lemmas (#20885) This PR adds a few lemmas about matroid closure, and its interaction with restrictions, independence and bases.

Estimated changes

Modified Mathlib/Data/Matroid/Closure.lean

added theorem Matroid.Basis.base_of_spanning

added theorem Matroid.Basis.closure_inter_basis_closure

added theorem Matroid.Basis.insert_basis_insert_of_not_mem_closure

added theorem Matroid.Basis.spanning_iff_spanning

added theorem Matroid.Indep.eq_of_spanning_subset

added theorem Matroid.Indep.exists_base_subset_spanning

added theorem Matroid.Indep.inter_Basis_biInter

added theorem Matroid.Indep.inter_Basis_iInter

added theorem Matroid.Indep.inter_Basis_sInter

added theorem Matroid.Indep.inter_basis_closure_iff_subset_closure_inter

added theorem Matroid.Indep.union_indep_iff_forall_not_mem_closure_left

added theorem Matroid.Indep.union_indep_iff_forall_not_mem_closure_right

added theorem Matroid.Restriction.base_iff_of_spanning

added theorem Matroid.Spanning.base_restrict_iff

added theorem Matroid.Spanning.compl_coindep

added theorem Matroid.closure_empty_eq_ground_iff

added theorem Matroid.closure_insert_congr_right

added theorem Matroid.closure_union_congr_left

added theorem Matroid.closure_union_congr_right

added theorem Matroid.comap_closure_eq

added theorem Matroid.emptyOn_closure_eq

added theorem Matroid.freeOn_closure_eq

added theorem Matroid.loopyOn_closure_eq

added theorem Matroid.loopyOn_spanning_iff

added theorem Matroid.map_closure_eq

added theorem Matroid.restrict_closure_eq'

added theorem Matroid.restrict_closure_eq

added theorem Matroid.restrict_spanning_iff'

added theorem Matroid.restrict_spanning_iff

added theorem Matroid.uniqueBaseOn_closure_eq