Commit 2026-02-11 17:08 77246884
View on Github →feat(Order/Filter/AtTopBot): use to_dual (#35133)
This PR generates Filter.atBot from Filter.atTop using to_dual.
atTop_eq_generate_of_forall_exists_le and atTop_eq_generate_of_not_bddAbove did not previously have a dual version.
Monotone.piecewise_eventually_eq_iUnion and Antitone.piecewise_eventually_eq_iInter do not have a name that distinguishes it from its dual version. Hence, I did not give it a to_dual tag.