mem_nhds_uniformity_iff_right — Mathlib

English

A neighborhood of x in the uniform topology can be characterized by right projections: s ∈ nhds x iff {p: α×α | p1 = x → p2 ∈ s} is in the uniformity.

Русский

Окрестность x в равномерной топологии задаётся через правая проекция: s ∈ nhds x тогда и только тогда, когда множество {p ∈ α×α : p1 = x → p2 ∈ s} принадлежит равномерности.

LaTeX

$$$s \in \mathcal N(x) \iff \{ p \in \alpha \times \alpha \mid p_1 = x \rightarrow p_2 \in s \} \in \mathcal U(\alpha)$$$

Lean4

theorem mem_nhds_uniformity_iff_right {x : α} {s : Set α} : s ∈ 𝓝 x ↔ {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α := by
  simp only [nhds_eq_comap_uniformity, mem_comap_prodMk]

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