Mathlib Changelog
v4
Changelog
About
Github
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