nhdsWithin_eq_comap_uniformity — Mathlib

English

For S ⊆ α, x ∈ α, the neighborhood within S is the comap of (𝓤 α ∩ 𝓟 (univ × S)) via x.

Русский

Для S ⊆ α и x ∈ α окрестности внутри S равны образу обратного направления от (𝓤 α ∩ 𝓟(univ × S)) через x.

LaTeX

$$$\mathcal N_S(x) = (\mathcal U(\alpha) \cap \mathcal P(\mathrm{univ} \times S)) \mathrm{comap} (\mathrm{Prod.mk}\ x)$$$

Lean4

theorem nhdsWithin_eq_comap_uniformity {x : α} (S : Set α) : 𝓝[S] x = (𝓤 α ⊓ 𝓟 (univ ×ˢ S)).comap (Prod.mk x) :=
  nhdsWithin_eq_comap_uniformity_of_mem (mem_univ _) S

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