Commit 2025-12-09 04:22 e9a19f30

View on Github →

chore(Order/WithBot): add to_dual attributes (part 1) (#32498)

Estimated changes

deleted def Equiv.withTopCongr
deleted theorem Equiv.withTopCongr_refl
deleted theorem Equiv.withTopCongr_symm
deleted theorem Equiv.withTopCongr_trans
modified theorem WithBot.coe_eq_top
modified theorem WithBot.coe_top
modified theorem WithBot.coe_unbot
modified theorem WithBot.map_comp_map
modified theorem WithBot.map₂_bot_left
modified theorem WithBot.map₂_bot_right
modified theorem WithBot.map₂_coe_coe
modified theorem WithBot.map₂_coe_left
modified theorem WithBot.map₂_coe_right
modified theorem WithBot.map₂_eq_bot_iff
modified theorem WithBot.top_eq_coe
deleted theorem WithTop.bot_eq_coe
deleted theorem WithTop.coe_bot
deleted theorem WithTop.coe_eq_bot
deleted theorem WithTop.coe_eq_coe
deleted theorem WithTop.coe_inj
deleted theorem WithTop.coe_injective
deleted theorem WithTop.coe_ne_top
deleted theorem WithTop.coe_untop
deleted theorem WithTop.comp_map
deleted theorem WithTop.eq_untop_iff
deleted theorem WithTop.exists_ne_top
deleted theorem WithTop.forall_ne_top
deleted def WithTop.map
deleted theorem WithTop.map_coe
deleted theorem WithTop.map_comm
deleted theorem WithTop.map_comp_map
deleted theorem WithTop.map_eq_some_iff
deleted theorem WithTop.map_eq_top_iff
deleted theorem WithTop.map_id
deleted theorem WithTop.map_injective
deleted theorem WithTop.map_map
deleted theorem WithTop.map_top
deleted def WithTop.map₂
deleted theorem WithTop.map₂_coe_coe
deleted theorem WithTop.map₂_coe_left
deleted theorem WithTop.map₂_coe_right
deleted theorem WithTop.map₂_eq_top_iff
deleted theorem WithTop.map₂_top_left
deleted theorem WithTop.map₂_top_right
deleted theorem WithTop.ne_top_iff_exists
deleted theorem WithTop.none_eq_top
deleted theorem WithTop.some_eq_coe
deleted theorem WithTop.some_eq_map_iff
deleted theorem WithTop.top_ne_coe
deleted def WithTop.untop
deleted theorem WithTop.untopA_eq_untop
deleted def WithTop.untopD
deleted theorem WithTop.untopD_coe
deleted theorem WithTop.untopD_eq_iff
deleted theorem WithTop.untopD_top
deleted theorem WithTop.untop_coe
deleted theorem WithTop.untop_eq_iff