Commit 2025-02-11 06:35 2b00f62e

View on Github →

feat(Order/Nucleus): nuclei form a frame (#21560) The nuclei form a heyting algebra and therefore a frame.

Estimated changes

Modified Mathlib/Order/Nucleus.lean

added theorem Nucleus.himp_apply

added theorem Nucleus.inf_apply

added theorem Nucleus.map_himp_apply

added theorem Nucleus.map_himp_le