Commit 2024-07-22 17:39 d995afc8

View on Github →

feat(Data/Matroid/Closure): matroid closure and independence (#15025) A bunch of API for the interaction between matroid closure and independence/bases.

Estimated changes

Modified Mathlib/Data/Matroid/Closure.lean

added theorem Matroid.Base.closure_eq

added theorem Matroid.Base.closure_of_superset

added theorem Matroid.Basis'.basis_closure_right

added theorem Matroid.Basis'.closure_eq_closure

added theorem Matroid.Basis.basis_closure_right

added theorem Matroid.Basis.basis_of_closure_eq_closure

added theorem Matroid.Basis.closure_eq_closure

added theorem Matroid.Basis.closure_eq_right

added theorem Matroid.Basis.eq_of_closure_subset

added theorem Matroid.Basis.subset_closure

added theorem Matroid.Indep.base_iff_ground_subset_closure

added theorem Matroid.Indep.base_of_ground_subset_closure

added theorem Matroid.Indep.basis_closure

added theorem Matroid.Indep.basis_of_subset_of_subset_closure

added theorem Matroid.Indep.closure_eq_setOf_basis_insert

added theorem Matroid.Indep.closure_iInter_eq_biInter_closure_of_forall_subset

added theorem Matroid.Indep.closure_inter_eq_inter_closure

added theorem Matroid.Indep.closure_inter_eq_self_of_subset

added theorem Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset

added theorem Matroid.Indep.insert_basis_iff_mem_closure

added theorem Matroid.Indep.insert_dep_iff

added theorem Matroid.Indep.insert_diff_indep_iff

added theorem Matroid.Indep.insert_indep_iff

added theorem Matroid.Indep.insert_indep_iff_of_not_mem

added theorem Matroid.Indep.mem_closure_iff'

added theorem Matroid.Indep.mem_closure_iff

added theorem Matroid.Indep.mem_closure_iff_of_not_mem

added theorem Matroid.Indep.not_mem_closure_iff

added theorem Matroid.Indep.not_mem_closure_iff_of_not_mem

added theorem Matroid.base_iff_indep_closure_eq

added theorem Matroid.basis'_iff_basis_closure

added theorem Matroid.basis_iff_basis_closure_of_subset'

added theorem Matroid.basis_iff_basis_closure_of_subset

added theorem Matroid.basis_iff_indep_closure

added theorem Matroid.basis_iff_indep_subset_closure

added theorem Matroid.basis_union_iff_indep_closure

added theorem Matroid.closure_biInter_eq_biInter_closure_of_biUnion_indep

added theorem Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep

added theorem Matroid.closure_sInter_eq_biInter_closure_of_sUnion_indep

added theorem Matroid.empty_basis_iff

added theorem Matroid.exists_basis_inter_ground_basis_closure

added theorem Matroid.insert_indep_iff