Commit 2026-02-22 23:38 baa59365

View on Github ā†’

chore: use @[to_dual] in Bounds/Image (#35211) This PR adds @[to_dual] annotations to primal theorems in Mathlib.Order.Bounds.Image, auto-generating their dual counterparts and deleting the hand-written versions. Covers MonotoneOn, AntitoneOn, Monotone, Antitone, image2, IsCofinalFor, Prod, and Pi sections. [Diff relative to #35208](https://github.com/kim-em/mathlib4/compare/kim/to-dual-bounds-basic...kim/to-dual-bounds-image)

  • depends on: #35208 šŸ¤– Prepared with Claude Code

Estimated changes

deleted theorem Antitone.map_bddBelow
deleted theorem Antitone.map_isLeast
deleted theorem AntitoneOn.map_bddBelow
deleted theorem AntitoneOn.map_isLeast
deleted theorem BddAbove.image2_bddBelow
deleted theorem BddBelow.range_comp
deleted theorem BddBelow.range_mono
deleted theorem IsGreatest.isLeast_image2
deleted theorem IsLUB.of_image
deleted theorem Monotone.map_bddBelow
deleted theorem Monotone.map_isGreatest
deleted theorem MonotoneOn.map_bddBelow
deleted theorem MonotoneOn.map_isGreatest
deleted theorem bddBelow_pi
deleted theorem bddBelow_prod
deleted theorem bddBelow_range_pi
deleted theorem bddBelow_range_prod
deleted theorem isGLB_pi
deleted theorem isGLB_prod
deleted theorem mem_lowerBounds_image2