Commit 2024-07-20 01:02 9417ef3e

View on Github →

feat(Data/Matroid/Closure): matroid closure (#14197) This PR defines the closure of a set in a matroid, and provides some API.

Estimated changes

added theorem Matroid.Flat.closure
added theorem Matroid.Flat.iInter
added structure Matroid.Flat
added def Matroid.closure
added theorem Matroid.closure_def'
added theorem Matroid.closure_def
added theorem Matroid.closure_ground
added theorem Matroid.closure_mono
added theorem Matroid.closure_univ
added theorem Matroid.ground_flat
added theorem Matroid.subset_closure