Commit 2025-04-02 15:28 c3148450

View on Github →

feat(Order/Filter/Ultrafilter/Basic): generalize lemma (#23569) Generalizes Filter.atTop_eq_pure_of_isTop and Filter.atBot_eq_pure_of_isBot from linear orders to partial orders.

Estimated changes