Commit 2023-01-16 11:30 09a26db3

View on Github →

feat: port Data.Set.Constructions (#1585)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Constructions.lean

added inductive FiniteInter.finiteInterClosure

added theorem FiniteInter.finiteInterClosure_FiniteInter

added theorem FiniteInter.finiteInterClosure_insert

added theorem FiniteInter.finiteInter_mem

added structure FiniteInter