Commit 2026-09-03 13:27 bf543ce7
View on Github →chore(Order/liminfLimsup): use to_dual (#37757)
This PR uses to_dual on limsup/liminf, and on some prerequisites.
Renames bliminf_antitone to bliminf_anti.
Deprecates bliminf_sup_le_inf_aux_left and bliminf_sup_le_inf_aux_right in favour of the stronger blimsup_and_le_inf. blimsup_and_le_inf has now been proved by apply_rw, which is a nice use of apply_rw, and I think the first one in mathlib.