Commit 2025-12-26 18:30 34426f49

View on Github →

refactor(Order/BoundedOrder/Lattice): use to_dual (#33268) It seems that this file has long lost its original purpose, so we also update the module docstring, and move some unrelated theorems to an earlier import.

Estimated changes

deleted theorem bot_inf_eq
modified theorem bot_sup_eq
deleted theorem exists_ge_and_iff_exists
deleted theorem exists_le_and_iff_exists
deleted theorem inf_bot_eq
deleted theorem inf_eq_top_iff
deleted theorem inf_top_eq
modified theorem max_bot_left
modified theorem max_bot_right
modified theorem max_eq_bot
deleted theorem max_eq_top
deleted theorem max_ne_top
deleted theorem max_top_left
deleted theorem max_top_right
modified theorem min_bot_left
modified theorem min_bot_right
modified theorem min_eq_bot
deleted theorem min_eq_top
added theorem min_ne_bot
deleted theorem min_top_left
deleted theorem min_top_right
modified theorem sup_bot_eq
modified theorem sup_top_eq
deleted theorem top_inf_eq
modified theorem top_sup_eq