Commit 2022-12-17 23:34 22fb95d2

View on Github →

feat: port Data.Set.Intervals.WithBotTop (#1072)

Estimated changes

Modified Mathlib.lean

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

added theorem WithBot.image_coe_Icc

added theorem WithBot.image_coe_Ici

added theorem WithBot.image_coe_Ico

added theorem WithBot.image_coe_Iic

added theorem WithBot.image_coe_Iio

added theorem WithBot.image_coe_Ioc

added theorem WithBot.image_coe_Ioi

added theorem WithBot.image_coe_Ioo

added theorem WithBot.preimage_coe_Icc

added theorem WithBot.preimage_coe_Ici

added theorem WithBot.preimage_coe_Ico

added theorem WithBot.preimage_coe_Iic

added theorem WithBot.preimage_coe_Iio

added theorem WithBot.preimage_coe_Ioc

added theorem WithBot.preimage_coe_Ioc_bot

added theorem WithBot.preimage_coe_Ioi

added theorem WithBot.preimage_coe_Ioi_bot

added theorem WithBot.preimage_coe_Ioo

added theorem WithBot.preimage_coe_Ioo_bot

added theorem WithBot.preimage_coe_bot

added theorem WithBot.range_coe

added theorem WithTop.image_coe_Icc

added theorem WithTop.image_coe_Ici

added theorem WithTop.image_coe_Ico

added theorem WithTop.image_coe_Iic

added theorem WithTop.image_coe_Iio

added theorem WithTop.image_coe_Ioc

added theorem WithTop.image_coe_Ioi

added theorem WithTop.image_coe_Ioo

added theorem WithTop.preimage_coe_Icc

added theorem WithTop.preimage_coe_Ici

added theorem WithTop.preimage_coe_Ico

added theorem WithTop.preimage_coe_Ico_top

added theorem WithTop.preimage_coe_Iic

added theorem WithTop.preimage_coe_Iio

added theorem WithTop.preimage_coe_Iio_top

added theorem WithTop.preimage_coe_Ioc

added theorem WithTop.preimage_coe_Ioi

added theorem WithTop.preimage_coe_Ioo

added theorem WithTop.preimage_coe_Ioo_top

added theorem WithTop.preimage_coe_top

added theorem WithTop.range_coe