mem_nhds_uniformity_iff_left — Mathlib

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]

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