Commit 2022-12-17 23:54 41bff331

View on Github →

feat: port Data.Set.Intervals.Group (#1038)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Monoid/Defs.lean

Created Mathlib/Data/Set/Intervals/Group.lean

added theorem Set.add_mem_Icc_iff_left

added theorem Set.add_mem_Icc_iff_right

added theorem Set.add_mem_Ico_iff_left

added theorem Set.add_mem_Ico_iff_right

added theorem Set.add_mem_Ioc_iff_left

added theorem Set.add_mem_Ioc_iff_right

added theorem Set.add_mem_Ioo_iff_left

added theorem Set.add_mem_Ioo_iff_right

added theorem Set.inv_mem_Icc_iff

added theorem Set.inv_mem_Ico_iff

added theorem Set.inv_mem_Ioc_iff

added theorem Set.inv_mem_Ioo_iff

added theorem Set.mem_Icc_iff_abs_le

added theorem Set.nonempty_Ico_sdiff

added theorem Set.sub_mem_Icc_iff_left

added theorem Set.sub_mem_Icc_iff_right

added theorem Set.sub_mem_Ico_iff_left

added theorem Set.sub_mem_Ico_iff_right

added theorem Set.sub_mem_Ioc_iff_left

added theorem Set.sub_mem_Ioc_iff_right

added theorem Set.sub_mem_Ioo_iff_left

added theorem Set.sub_mem_Ioo_iff_right