mathlib

894f92bc - refactor(order/upper_lower): Reverse the order on `upper_set` (#14982)

refactor(order/upper_lower): Reverse the order on `upper_set` (#14982) Having `upper_set` being ordered by reverse inclusion makes it order-isomorphic to `lower_set` (and antichains once we have them as a type) and it matches the order on `filter`.