English
There is a natural category structure on OpenNhds x: objects are open neighborhoods of x and morphisms are inclusion-respecting maps between them.
Русский
Существуют естественные структура категории для OpenNhds x: объекты — открытые окрестности x, морфизмы — отображения, сохраняющие вложения.
LaTeX
$$OpenNhds x is a category with objects $U$ and morphisms $U\\to V$ given by inclusions.$$
Lean4
instance (x : X) : Lattice (OpenNhds x) :=
{ OpenNhds.partialOrder x with
inf := fun U V => ⟨U.1 ⊓ V.1, ⟨U.2, V.2⟩⟩
le_inf := fun U V W => @le_inf _ _ U.1.1 V.1.1 W.1.1
inf_le_left := fun U V => @inf_le_left _ _ U.1.1 V.1.1
inf_le_right := fun U V => @inf_le_right _ _ U.1.1 V.1.1
sup := fun U V => ⟨U.1 ⊔ V.1, Set.mem_union_left V.1.1 U.2⟩
sup_le := fun U V W => @sup_le _ _ U.1.1 V.1.1 W.1.1
le_sup_left := fun U V => @le_sup_left _ _ U.1.1 V.1.1
le_sup_right := fun U V => @le_sup_right _ _ U.1.1 V.1.1 }
