Theorem monotone_id

Modification history

2022-11-22 07:59

Mathlib/Order/Monotone.lean

feat: add `fun x ↦ t` syntax (#617)

Modified monotone_id View on Github →

2022-09-30 18:50

Mathlib/Order/Monotone.lean

feat: port order/monotone, needed for apply_fun (#441)

Added monotone_id View on Github →