English
Let t be a subset of a topological space X. If the set-neighborhood filter 𝓝ˢ t has a basis {s_i} with index i in I and a predicate p(i), then the family { interior(s_i) } (i ∈ I) also forms a basis for 𝓝ˢ t with the same predicate.
Русский
Пусть t ⊆ X и пространство X имеет топологию. Если фильтр множество окрестностей 𝓝ˢ t имеет базис {s_i} с индексами i∈I и свойством p(i), то семейство { interior(s_i) } той же индексации образует базис 𝓝ˢ t с тем же условием.
LaTeX
$$$ (𝓝ˢ t).HasBasis p s \Rightarrow (𝓝ˢ t).HasBasis p (fun i => interior (s i)) $$$
Lean4
theorem nhdsSet_interior {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {t : Set X} (h : (𝓝ˢ t).HasBasis p s) :
(𝓝ˢ t).HasBasis p (interior <| s ·) :=
lift'_nhdsSet_interior t ▸ h.lift'_interior
