Commit 2024-04-05 12:26 18605548

View on Github →

feat: add missing Set.Ioo_inter_Iio etc (#11902) add missing lemmas. I'm not sure if these should be @[simp], as e.g. Ico_inter_Ico isn't, but Ico_inter_Iio is

Estimated changes

Modified Mathlib/Data/Set/Intervals/Basic.lean

added theorem Set.Iio_inter_Ioo

added theorem Set.Ioi_inter_Ioo

added theorem Set.Ioo_inter_Iio

added theorem Set.Ioo_inter_Ioi