Commit 2025-04-14 15:20 692dd556
View on Github →feat(Order/Nucleus): The image of a nucleus is a frame (#23802) The image of a nucleus is a frame (which is the sublocale corresponding to this nucleus). If we restrict the codomain of a nucleus to its image, it is a FrameHom.