Theorem Monotone.of_map_inf_le

Modification history

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_leView on Github →