English
The restriction map n.restrict : X → range(n) (given by x ↦ rangeFactorization n x) is a frame homomorphism from X to the subframe range(n).
Русский
Ограничение нуклеуса n до диапазона n, получающееся по карте x ↦ rangeFactorization n x, является гомоморфизмом рам от X к подраме range(n).
LaTeX
$$$\\operatorname{restrict}(n) : X \\to \\operatorname{range}(n) \\text{ is a frame homomorphism.}$$$
Lean4
/-- Restrict a nucleus to its range. -/
@[simps]
def restrict (n : Nucleus X) : FrameHom X (range n)
where
toFun := rangeFactorization n
map_inf' a b := by ext; exact map_inf
map_top' := by ext; exact map_top n
map_sSup' s := by rw [n.giAux.gc.l_sSup, sSup_image]
