mem_nhds_left — Mathlib

English

Let α be a uniform space and x be a point of α. For every entourage s in the uniformity 𝓤 α, the set { y ∈ α | (x, y) ∈ s } is a neighborhood of x, i.e., belongs to 𝓝 x.

Русский

Пусть α — равномерное пространство и x ∈ α. Для каждого окружения s ∈ 𝓤 α множество { y ∈ α | (x, y) ∈ s } является окрестностью x, то есть принадлежит 𝓝 x.

LaTeX

$$$\forall x : α, ∀ s ∈ 𝓤 α, { y : α \mid (x, y) ∈ s } ∈ 𝓝 x$$$

Lean4

theorem mem_nhds_left (x : α) {s : Set (α × α)} (h : s ∈ 𝓤 α) : {y : α | (x, y) ∈ s} ∈ 𝓝 x :=
  ball_mem_nhds x h

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