Theorem constant_of_monotone_antitone

Modification history

2025-12-08 05:19
Mathlib/Order/Directed.lean
refactor: make `abbrev`s for `IsDirected α (· ≤ ·)` and `IsDirected α (· ≥ ·)` (#32462) …
Modified constant_of_monotone_antitoneView on Github →
2024-02-13 15:17
Mathlib/Order/Directed.lean
feat(Topology/Algebra/Order): continuous injective function on interval is strictly monotone (#7018) …
Added constant_of_monotone_antitoneView on Github →