Commit 2025-01-01 21:51 12bb04fb

feat: add Set.preimage_image_univ and associated GaloisConnection result (#20346) this function shows that the preimage of the image of a universal set is the universal set. Since preimage and image form a Galois connection, this is a special case of a more general theorem that I added there. I chose not to use the general theorem in the special theorem since doing so would require either putting the preimage_image_univ function in an unnatural spot or solving a circular import problem.