Commit 2024-10-22 08:37 25461520

View on Github →

feat(Data/Matroid/Closure): closure + insertion API (#15028) Some API for interactions between independence, closure and single-element insertions/differences in matroids.

Estimated changes

Modified Mathlib/Data/Matroid/Closure.lean

added theorem Matroid.Indep.closure_diff_singleton_ssubset

added theorem Matroid.Indep.closure_diff_ssubset

added theorem Matroid.Indep.closure_ssubset_closure

added theorem Matroid.Indep.not_mem_closure_diff_of_mem

added theorem Matroid.closure_diff_eq_self

added theorem Matroid.closure_diff_singleton_eq_closure

added theorem Matroid.closure_exchange

added theorem Matroid.closure_exchange_iff

added theorem Matroid.closure_insert_congr

added theorem Matroid.ext_closure

added theorem Matroid.indep_iff_forall_closure_diff_ne

added theorem Matroid.indep_iff_forall_closure_ssubset_of_ssubset

added theorem Matroid.indep_iff_forall_not_mem_closure_diff'

added theorem Matroid.indep_iff_forall_not_mem_closure_diff

added theorem Matroid.mem_closure_diff_singleton_iff_closure

added theorem Matroid.mem_closure_insert

added theorem Matroid.subset_closure_diff_iff_closure_eq