Mathlib v3 is deprecated. Go to Mathlib v4

Theorem directed_on_range

Modification history

2023-04-20 22:04
src/order/directed.lean
feat(order/compactly_generated): For any `b`, there exists a set of independent atoms `s` such that `Sup s` is the complement of `b`. (#8475) …
Modified directed_on_rangeView on Github →
2023-01-03 06:58
src/order/directed.lean
feat(category_theory/mittag_leffler): Introduce the Mittag-Leffler condition (#17905) …
Added directed_on_rangeView on Github →