Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

added theorem Inf_image2
added theorem Sup_image2
added theorem binfi_prod
added theorem bsupr_prod
modified theorem infi_prod
modified theorem supr_prod