Theorem Monotone.comp_antitone

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 Monotone.comp_antitone View on Github →

2022-10-17 21:30

Mathlib/Order/Monotone.lean

feat: port Algebra/CovariantAndContravariant (#467) …

Added Monotone.comp_antitone View on Github →