Theorem Monotone.disjointed_succ_sup

Modification history

2025-01-21 20:44
Mathlib/Order/Disjointed.lean
refactor(Order/Disjointed): allow arbitrary partial orders as domain (#20545)
Added Monotone.disjointed_succ_supView on Github →