localePointOfSpacePoint — Mathlib

English

The unit of the adjunction sends a point x ∈ X to the corresponding point of Opens X given by U ↦ [x ∈ U].

Русский

Единица сопряжения отправляет точку x ∈ X в соответствующую точку открытых подмножеств X, заданную U ↦ [x ∈ U].

LaTeX

$$localePointOfSpacePoint(X,x) : PT (Opens X) with toFun = (x ∈ ·)$$

Lean4

/-- The unit of the adjunction between locales and topological spaces, which associates with
a point `x` of the space `X` a point of the locale of opens of `X`. -/
@[simps]
def localePointOfSpacePoint (x : X) : PT (Opens X)
    where
  toFun := (x ∈ ·)
  map_inf' _ _ := rfl
  map_top' := rfl
  map_sSup' S := by simp [«Prop».exists_iff]

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