mathlib3

0c171f29 - feat(order/upper_lower): Product of upper sets (#17022)

feat(order/upper_lower): Product of upper sets (#17022) Define the product of two upper/lower sets as an upper/lower set. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>