Commit 2026-09-07 15:38 4d65fcff

View on Github →

chore(Order): use to_dual in various places (#43323) This PR uses to_dual for various order theorems.

Estimated changes

Modified Mathlib/Order/Bounded.lean

deleted theorem Set.unbounded_ge_iff

deleted theorem Set.unbounded_ge_of_forall_exists_gt

deleted theorem Set.unbounded_gt_iff

deleted theorem Set.unbounded_gt_of_forall_exists_ge

Modified Mathlib/Order/BoundedOrder/Monotone.lean

deleted theorem StrictAnti.apply_eq_bot_iff

deleted theorem StrictMono.apply_eq_bot_iff

deleted theorem StrictMono.minimal_preimage_bot

Modified Mathlib/Order/Bounds/Image.lean

deleted theorem StrictAnti.map_isGreatest

deleted theorem StrictAnti.mem_lowerBounds_image

deleted theorem StrictMono.map_isGreatest

deleted theorem StrictMono.mem_lowerBounds_image

Modified Mathlib/Order/Bounds/OrderIso.lean

deleted theorem OrderIso.isGLB_image'

deleted theorem OrderIso.isGLB_image

deleted theorem OrderIso.isGLB_preimage'

deleted theorem OrderIso.isGLB_preimage

deleted theorem OrderIso.lowerBounds_image

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

deleted theorem iSup_iInf_le

Modified Mathlib/Order/Filter/AtTopBot/Map.lean

deleted theorem OrderIso.comap_atBot

deleted theorem OrderIso.map_atBot

deleted theorem OrderIso.tendsto_atBot

deleted theorem OrderIso.tendsto_atBot_iff

Modified Mathlib/Order/SuccPred/CompleteLinearOrder.lean

deleted theorem exists_eq_iInf_of_not_isPredPrelimit

deleted theorem sInf_mem_of_not_isPredPrelimit