Theorem Monotone.of_map_inf_le

Modification history

2026-03-23 08:24

Mathlib/Order/Lattice.lean

chore(Order/Lattice): use `to_dual` for lemmas about `Monotone` (#37005)

Deleted Monotone.of_map_inf_le View on Github →

2024-09-03 09:13

Mathlib/Order/Lattice.lean

feat(Order/Lattice): add Monotone.of_map_inf_le_left etc (#15508) …

Added Monotone.of_map_inf_le View on Github →