feat(order/bounds): Bounds on `set.image2` (#14306)
feat(order/bounds): Bounds on `set.image2` (#14306)

`set.image2` analogues to the `set.image` lemmas.





leanprover-community/mathlib,leanprover-community/mathlib