nhdsWithin_eq_comap_uniformity_of_mem

English

If x ∈ T, then the neighborhood filter of x relative to T equals the comap of the intersection of the uniformity with the principal filter on T × S by the map x ↦ (x,).

Русский

Если x ∈ T, то окрестности x в пределах T равны образу обратного направления от пересечения равномерности и принципиального фильтра на T × S по карте x ↦ (x).

LaTeX

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

Lean4

theorem nhdsWithin_eq_comap_uniformity_of_mem {x : α} {T : Set α} (hx : x ∈ T) (S : Set α) :
    𝓝[S] x = (𝓤 α ⊓ 𝓟 (T ×ˢ S)).comap (Prod.mk x) := by simp [nhdsWithin, nhds_eq_comap_uniformity, hx]

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