Theorem inf_supₛ_eq_of_directedOn

Modification history

2023-04-28 11:44
Mathlib/Order/CompactlyGenerated.lean
feat: For any `b`, there exists a set `s` of independent atoms such that `Sup s` is the complement of `b` (#3588) …
Deleted inf_supₛ_eq_of_directedOnView on Github →
2023-02-01 13:07
Mathlib/Order/CompactlyGenerated.lean
feat: port Order.CompactlyGenerated (#1976) …
Added inf_supₛ_eq_of_directedOnView on Github →