English
For any nucleus n on a frame X, the carrier of its associated sublocale is the range of n; i.e., the range of a nucleus forms a sublocale of X.
Русский
Для нуклеуса n на рамке X множество-носитель соответствующей сублокалы образуется наложением диапазона n; то есть образ нуклеуса образует сублокалю X.
LaTeX
$$$\operatorname{range}(n)\text{ is a Sublocale}(X)$$$
Lean4
/-- The range of a nucleus is a sublocale. -/
@[simps]
def toSublocale (n : Nucleus X) : Sublocale X where
carrier := range n
sInf_mem' a
h := by
rw [mem_range]
refine le_antisymm (le_sInf_iff.mpr (fun b h1 ↦ ?_)) le_apply
simp_rw [subset_def, mem_range] at h
rw [← h b h1]
exact n.monotone (sInf_le h1)
himp_mem' a b h := by rw [mem_range, ← h, map_himp_apply] at *
