toNucleus — Mathlib

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 _

Похожие утверждения