ball_mem_nhdsWithin — Mathlib

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⟩

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