restrict_toSublocale — Mathlib

English

Restricting the sublocale associated to a nucleus n to a point x yields the triple ⟨n(x), x, rfl⟩.

Русский

Ограничение сублокалы, ассоциированной с нуклеусом n, к точке x даёт тройку ⟨n(x), x, rfl⟩.

LaTeX

$$$(n^{\mathrm{toSublocale}}).\mathrm{restrict}(x) = \langle n(x), x, rfl\rangle$$$

Lean4

@[simp]
theorem restrict_toSublocale (n : Nucleus X) (x : X) : n.toSublocale.restrict x = ⟨n x, x, rfl⟩ :=
  by
  ext
  simpa [Sublocale.restrict, sInf_image, le_antisymm_iff (a := iInf _)] using
    ⟨iInf₂_le_of_le ⟨n x, x, rfl⟩ n.le_apply le_rfl, fun y hxy ↦ by simpa using n.monotone hxy⟩

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