mathlib3
5d18a722 - feat(order/{conditionally_complete_lattice,galois_connection): Supremum of `set.image2` (#14307)

Commit

3 years ago

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.

Author

YaelDillies

Parents

300c4395

mathlib3 5d18a722 - feat(order/{conditionally_complete_lattice,galois_connection): Supremum of `set.image2` (#14307)

mathlib3
5d18a722 - feat(order/{conditionally_complete_lattice,galois_connection): Supremum of `set.image2` (#14307)