mem_nhds_right — Mathlib

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)

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