Theorem directedOn_range

Modification history

2023-04-28 11:44
Mathlib/Order/Directed.lean
feat: For any `b`, there exists a set `s` of independent atoms such that `Sup s` is the complement of `b` (#3588) …
Modified directedOn_rangeView on Github →
2023-01-05 03:18
Mathlib/Order/Directed.lean
feat: synchronize with mathlib3 #17905 (#1280) …
Added directedOn_rangeView on Github →