Commit 2025-05-07 09:33 0371bcab

feat(Order): directed products and upper bounds (#21493) A collection of lemmas building to Monotone.upperBounds_image_of_directedOn_prod - the upper bounds of the image of a directed product space coincide with the upper bounds of the image of the product of the components. I have also included lowerBounds lemmas where appropriate for completeness.