English
A left-variant characterization: s ∈ nhds x iff {p: α×α | p2 = x → p1 ∈ s} ∈ 𝓤 α.
Русский
Левая версия: s ∈ nhds x тогда и только тогда, когда {p: α×α | p2 = x → p1 ∈ s} ∈ 𝓤 α.
LaTeX
$$$s \in \mathcal N(x) \iff \{ p \in \alpha \times \alpha \mid p_2 = x \rightarrow p_1 \in s \} \in \mathcal U(\alpha)$$$
Lean4
theorem mem_nhds_uniformity_iff_left {x : α} {s : Set α} : s ∈ 𝓝 x ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ 𝓤 α :=
by
rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right]
simp only [mem_map, preimage_setOf_eq, Prod.snd_swap, Prod.fst_swap]