Commit 2022-11-29 20:56 25f9f172

View on Github →

feat: port Order.WithBot (#777) SHA: 4674d16c9f219334f07b9220ea5f315838bbb573 Finished port The main change was introducing WithBot.some and WithTop.some and defining the coercion as WithBot.some instead of Option.some to avoid elaboration issues with using Option.some.

Estimated changes

added theorem WithBot.bot_lt_coe
added theorem WithBot.bot_ne_coe
added theorem WithBot.coe_eq_coe
added theorem WithBot.coe_inf
added theorem WithBot.coe_inj
added theorem WithBot.coe_injective
added theorem WithBot.coe_le
added theorem WithBot.coe_le_coe
added theorem WithBot.coe_le_iff
added theorem WithBot.coe_lt_coe
added theorem WithBot.coe_max
added theorem WithBot.coe_min
added theorem WithBot.coe_mono
added theorem WithBot.coe_ne_bot
added theorem WithBot.coe_sup
added theorem WithBot.coe_unbot
added theorem WithBot.le_coe_iff
added theorem WithBot.le_coe_unbot'
added theorem WithBot.le_ofDual_iff
added theorem WithBot.le_toDual_iff
added theorem WithBot.lt_coe_iff
added theorem WithBot.lt_ofDual_iff
added theorem WithBot.lt_toDual_iff
added def WithBot.map
added theorem WithBot.map_bot
added theorem WithBot.map_coe
added theorem WithBot.map_comm
added theorem WithBot.map_le_iff
added theorem WithBot.map_ofDual
added theorem WithBot.map_toDual
added theorem WithBot.monotone_iff
added theorem WithBot.none_eq_bot
added theorem WithBot.none_le
added theorem WithBot.none_lt_some
added theorem WithBot.not_coe_le_bot
added theorem WithBot.not_lt_none
added theorem WithBot.ofDual_le_iff
added theorem WithBot.ofDual_lt_iff
added theorem WithBot.ofDual_map
added def WithBot.some
added theorem WithBot.some_eq_coe
added theorem WithBot.some_le_some
added theorem WithBot.some_lt_some
added theorem WithBot.toDual_le_iff
added theorem WithBot.toDual_lt_iff
added theorem WithBot.toDual_map
added def WithBot.unbot'
added theorem WithBot.unbot'_bot
added theorem WithBot.unbot'_coe
added theorem WithBot.unbot'_lt_iff
added def WithBot.unbot
added theorem WithBot.unbot_coe
added def WithBot
added theorem WithTop.coe_eq_coe
added theorem WithTop.coe_inf
added theorem WithTop.coe_le_coe
added theorem WithTop.coe_le_iff
added theorem WithTop.coe_lt_coe
added theorem WithTop.coe_lt_iff
added theorem WithTop.coe_lt_top
added theorem WithTop.coe_max
added theorem WithTop.coe_min
added theorem WithTop.coe_mono
added theorem WithTop.coe_ne_top
added theorem WithTop.coe_sup
added theorem WithTop.coe_untop
added theorem WithTop.le_coe
added theorem WithTop.le_coe_iff
added theorem WithTop.le_none
added theorem WithTop.le_ofDual_iff
added theorem WithTop.le_toDual_iff
added theorem WithTop.lt_ofDual_iff
added theorem WithTop.lt_toDual_iff
added def WithTop.map
added theorem WithTop.map_coe
added theorem WithTop.map_comm
added theorem WithTop.map_le_iff
added theorem WithTop.map_ofDual
added theorem WithTop.map_toDual
added theorem WithTop.map_top
added theorem WithTop.monotone_iff
added theorem WithTop.none_eq_top
added theorem WithTop.not_none_lt
added theorem WithTop.not_top_le_coe
added theorem WithTop.ofDual_le_iff
added theorem WithTop.ofDual_lt_iff
added theorem WithTop.ofDual_map
added def WithTop.some
added theorem WithTop.some_eq_coe
added theorem WithTop.some_le_some
added theorem WithTop.some_lt_none
added theorem WithTop.some_lt_some
added theorem WithTop.toDual_le_iff
added theorem WithTop.toDual_lt_iff
added theorem WithTop.toDual_map
added theorem WithTop.top_ne_coe
added def WithTop.untop'
added theorem WithTop.untop'_coe
added theorem WithTop.untop'_top
added def WithTop.untop
added theorem WithTop.untop_coe
added def WithTop