# Commit 2022-06-14 13:35 5d18a722

View on Github →feat(order/{conditionally_complete_lattice,galois_connection): Supremum of `set.image2`

(#14307)
`Sup`

and `Inf`

distribute over `set.image2`

in the presence of appropriate Galois connections.

Mathlib v3 is deprecated. Go to Mathlib v4

feat(order/{conditionally_complete_lattice,galois_connection): Supremum of `set.image2`

(#14307)
`Sup`

and `Inf`

distribute over `set.image2`

in the presence of appropriate Galois connections.