English
If x ∈ S and V is in the intersection of the uniformity with the principal on S×S, then ball x V is in nhdsWithin x S.
Русский
Если x ∈ S и V лежит в пересечении равномерности и принципиального фильтра на S×S, то ball x V принадлежит nhdsWithin x S.
LaTeX
$$$(x \in S) \Rightarrow (V \in \mathcal U(\alpha) \cap \mathcal P(S \times S)) \Rightarrow \operatorname{ball}(x,V) \in \mathcal N_S(x)$$$
Lean4
theorem ball_mem_nhdsWithin {x : α} {S : Set α} ⦃V : Set (α × α)⦄ (x_in : x ∈ S) (V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)) :
ball x V ∈ 𝓝[S] x := by
rw [nhdsWithin_eq_comap_uniformity_of_mem x_in, mem_comap]
exact ⟨V, V_in, Subset.rfl⟩