Theorem Codisjoint.mono_left

Modification history

2025-12-24 12:03
Mathlib/Order/Disjoint.lean
feat(Order/Disjoint): use `@[to_dual]` (#33140) …
Deleted Codisjoint.mono_leftView on Github →
2025-07-31 09:17
Mathlib/Order/Disjoint.lean
feat(gcongr): also use more general lemmas, closing extra goals with rfl (#26907) …
Modified Codisjoint.mono_leftView on Github →
2025-06-11 22:43
Mathlib/Order/Disjoint.lean
feat: a `grw` tactic for rewriting using inequalities (#8167)
Modified Codisjoint.mono_leftView on Github →
2022-11-28 22:38
Mathlib/Order/Disjoint.lean
feat: port Order.Disjoint (#773) …
Added Codisjoint.mono_leftView on Github →