English
The range of the toNucleus map is exactly the sublocale S.
Русский
Область значений отображения toNucleus равна самой подлокали S.
LaTeX
$$$\operatorname{range}(S.toNucleus) = S$$$
Lean4
/-- The restriction from the locale X into a sublocale is a nucleus. -/
@[simps]
def toNucleus (S : Sublocale X) : Nucleus X where
toFun x := S.restrict x
map_inf' _ _ := by simp [S.giRestrict.gc.u_inf]
idempotent' _ := by rw [S.giRestrict.gc.l_u_l_eq_l]
le_apply' _ := S.giRestrict.gc.le_u_l _