Commit 2022-04-10 01:48 9495b8cb

View on Github →

feat(data/set/intervals/with_bot_top): lemmas about I?? and with_top/bot (#4273) Prove theorems about (pre)images of intervals under coe : α → with_top α and coe : α → with_bot α.

Estimated changes

Created src/data/set/intervals/with_bot_top.lean

added theorem with_bot.image_coe_Icc

added theorem with_bot.image_coe_Ici

added theorem with_bot.image_coe_Ico

added theorem with_bot.image_coe_Iic

added theorem with_bot.image_coe_Iio

added theorem with_bot.image_coe_Ioc

added theorem with_bot.image_coe_Ioi

added theorem with_bot.image_coe_Ioo

added theorem with_bot.preimage_coe_Icc

added theorem with_bot.preimage_coe_Ici

added theorem with_bot.preimage_coe_Ico

added theorem with_bot.preimage_coe_Iic

added theorem with_bot.preimage_coe_Iio

added theorem with_bot.preimage_coe_Ioc

added theorem with_bot.preimage_coe_Ioc_bot

added theorem with_bot.preimage_coe_Ioi

added theorem with_bot.preimage_coe_Ioi_bot

added theorem with_bot.preimage_coe_Ioo

added theorem with_bot.preimage_coe_Ioo_bot

added theorem with_bot.preimage_coe_bot

added theorem with_bot.range_coe

added theorem with_top.image_coe_Icc

added theorem with_top.image_coe_Ici

added theorem with_top.image_coe_Ico

added theorem with_top.image_coe_Iic

added theorem with_top.image_coe_Iio

added theorem with_top.image_coe_Ioc

added theorem with_top.image_coe_Ioi

added theorem with_top.image_coe_Ioo

added theorem with_top.preimage_coe_Icc

added theorem with_top.preimage_coe_Ici

added theorem with_top.preimage_coe_Ico

added theorem with_top.preimage_coe_Ico_top

added theorem with_top.preimage_coe_Iic

added theorem with_top.preimage_coe_Iio

added theorem with_top.preimage_coe_Iio_top

added theorem with_top.preimage_coe_Ioc

added theorem with_top.preimage_coe_Ioi

added theorem with_top.preimage_coe_Ioo

added theorem with_top.preimage_coe_Ioo_top

added theorem with_top.preimage_coe_top

added theorem with_top.range_coe