Theorem MaximalFor.maximal_of_strictMonoOn

Modification history

2026-04-08 17:43

Mathlib/Order/Minimal.lean

chore(Order/Minimal): use `to_dual` (#37732)

Deleted MaximalFor.maximal_of_strictMonoOn View on Github →

2026-01-31 20:13

Mathlib/Order/Minimal.lean

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

Added MaximalFor.maximal_of_strictMonoOn View on Github →