Commit 2026-01-31 20:13 bf85848f

View on Github →

feat(Order/Minimal): uncompose MinimalFor/MaximalFor with a strictly monotonic function (#34655)

Estimated changes

Modified Mathlib/Order/Minimal.lean

added theorem MaximalFor.maximal_of_strictMonoOn

added theorem MaximalFor.minimalFor_of_strictAntiOn_comp

added theorem MaximalFor.minimal_of_strictAntiOn

added theorem MaximalFor.of_strictMonoOn_comp

added theorem MinimalFor.maximalFor_of_strictAntiOn_comp

added theorem MinimalFor.maximal_of_strictAntiOn

added theorem MinimalFor.minimal_of_strictMonoOn

added theorem MinimalFor.of_strictMonoOn_comp