mem_nhds_iff — Mathlib

English

Characterizes membership of s in nhds x by the existence of a ball around x contained in s with a uniformity bound.

Русский

Характеризует принадлежность s окрестности x через существование шара вокруг x, содержащегося в s, с верхней границей равномерности.

LaTeX

$$$s \in \mathcal N(x) \iff \exists V \in \mathcal U(\alpha)\,\, (\operatorname{ball}(x,V) \subseteq s)$$$

Lean4

theorem mem_nhds_iff {x : α} {s : Set α} : s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s :=
  by
  rw [nhds_eq_comap_uniformity, mem_comap]
  simp_rw [ball]

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