Commit 2025-12-05 13:19 dbaea0e1

View on Github →

chore(Order/BoundedOrder/Basic): use to_dual (#32377) Notes:

  • eq_bot_of_minimal didn't have a dual version, and was unused, so I deprecated it.
  • I removed the two >6 month old deprecations.
  • The choice of whether to write down top/bot lemmas is mostly based on whichever one came first originally.

Estimated changes

deleted theorem Ne.bot_lt'
deleted theorem Ne.bot_lt
deleted theorem OrderDual.ofDual_bot
deleted theorem OrderDual.ofDual_eq_bot
modified theorem OrderDual.ofDual_eq_top
modified theorem OrderDual.ofDual_top
deleted theorem OrderDual.toDual_bot
deleted theorem OrderDual.toDual_eq_bot
modified theorem OrderDual.toDual_eq_top
modified theorem OrderDual.toDual_top
deleted theorem Pi.top_apply
deleted theorem Pi.top_comp
deleted theorem Pi.top_def
deleted theorem Prod.fst_bot
modified theorem Prod.fst_top
deleted theorem Prod.snd_bot
modified theorem Prod.snd_top
deleted theorem Subtype.coe_eq_top_iff
deleted theorem Subtype.coe_top
deleted theorem Subtype.mk_eq_top_iff
deleted theorem Subtype.mk_top
deleted theorem ULift.down_bot
modified theorem ULift.down_top
deleted theorem ULift.up_bot
modified theorem ULift.up_top
deleted theorem bot_le
deleted theorem bot_lt_iff_ne_bot
deleted theorem bot_lt_of_lt
deleted theorem bot_notMem_iff
deleted theorem bot_unique
deleted theorem eq_bot_iff
deleted theorem eq_bot_mono
deleted theorem eq_bot_or_bot_lt
deleted theorem isBot_bot
deleted theorem isBot_iff_eq_bot
deleted theorem isMin_bot
deleted theorem isMin_iff_eq_bot
deleted theorem le_bot_iff
modified theorem lt_top_of_lt
deleted theorem ne_bot_of_gt
deleted theorem ne_bot_of_le_ne_bot
deleted theorem not_bot_lt_iff
deleted theorem not_isBot_iff_ne_bot
deleted theorem not_isMax_bot
deleted theorem not_isMin_iff_ne_bot
deleted theorem not_lt_bot
deleted theorem top_ne_bot