English
Let α be a uniform space and y ∈ α. For any s ∈ 𝓤 α, the set { x ∈ α | (x, y) ∈ s } is a neighborhood of y, i.e., belongs to 𝓝 y.
Русский
Пусть α — равномерное пространство и y ∈ α. Для любого s ∈ 𝓤 α множество { x ∈ α | (x, y) ∈ s } принадлежит 𝓝 y.
LaTeX
$$$\forall y : α, ∀ s ∈ 𝓤 α, { x : α | (x, y) ∈ s } ∈ 𝓝 y$$$
Lean4
theorem mem_nhds_right (y : α) {s : Set (α × α)} (h : s ∈ 𝓤 α) : {x : α | (x, y) ∈ s} ∈ 𝓝 y :=
mem_nhds_left _ (symm_le_uniformity h)