Commit 2025-08-12 05:09 6559cf53

View on Github →

feat(Order/Sublocale): definition of sublocales (#25089) There are several possible definition of sublocales. I used one from nlab which states that a sublocale is a subset of a locale which is closed under all meets and for any s ∈ S and x ∈ X, we have (x ⇨ s) ∈ S. This PR also includes an order isomorphism between (Nucleus)ᵒᵈ and Sublocale.

Estimated changes

added theorem InfHom.mk_le_mk
added theorem SupHom.mk_le_mk
added theorem Nucleus.coe_inf
modified theorem Nucleus.himp_apply
modified theorem Nucleus.iInf_apply
modified theorem Nucleus.idempotent
modified theorem Nucleus.inf_apply
added theorem Nucleus.mk_le_mk
modified theorem Nucleus.sInf_apply
modified theorem Nucleus.toFun_eq_coe
added theorem Sublocale.coe_himp
added theorem Sublocale.coe_iInf
added theorem Sublocale.coe_inf
added theorem Sublocale.coe_sInf
added theorem Sublocale.ext
added theorem Sublocale.himp_mem
added theorem Sublocale.iInf_mem
added theorem Sublocale.infClosed
added theorem Sublocale.inf_mem
added theorem Sublocale.mem_carrier
added theorem Sublocale.mem_mk
added theorem Sublocale.mk_le_mk
added theorem Sublocale.sInf_mem
added theorem Sublocale.top_mem
added structure Sublocale
added theorem OrderDual.ext