Theorem strictMonoOn_id

Modification history

2025-02-18 13:54

Mathlib/Order/Monotone/Basic.lean

chore(Order/Monotone): split `Basic.lean` into `Basic.lean` and `Defs.lean` (#22004) …

Modified strictMonoOn_id View on Github →

2022-11-22 07:59

Mathlib/Order/Monotone.lean

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

Modified strictMonoOn_id View on Github →

2022-11-18 09:07

Mathlib/Order/Monotone.lean

feat: port Order.Monotone (#591) …

Added strictMonoOn_id View on Github →