mathlib3

22bdc8ec - feat(order/upper_lower): Upper/lower sets (#12189)

feat(order/upper_lower): Upper/lower sets (#12189) Define upper and lower sets both as unbundled predicates and as bundled types. Co-authored-by: Sara Rousta <@SaraRousta>