Theorem Codisjoint.mono

Modification history

2025-12-24 12:03

Mathlib/Order/Disjoint.lean

feat(Order/Disjoint): use `@[to_dual]` (#33140) …

Deleted Codisjoint.mono View on Github →

2025-06-11 22:43

Mathlib/Order/Disjoint.lean

feat: a `grw` tactic for rewriting using inequalities (#8167)

Modified Codisjoint.mono View on Github →

2022-11-28 22:38

Mathlib/Order/Disjoint.lean

feat: port Order.Disjoint (#773) …

Added Codisjoint.mono View on Github →