Theorem Antitone.comp_monotone

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 Antitone.comp_monotone View on Github →

2022-10-17 21:30

Mathlib/Order/Monotone.lean

feat: port Algebra/CovariantAndContravariant (#467) …

Added Antitone.comp_monotone View on Github →