English
Let s be an open set. Then s belongs to the set-neighborhoods filter 𝓝ˢ t if and only if t is contained in s.
Русский
Пусть s открыто. Тогда s принадлежит фильтру множеств-окрестностей 𝓝ˢ t тогда и только тогда, когда t ⊆ s.
LaTeX
$$$ IsOpen(s) \rightarrow (s \in 𝓝ˢ t \leftrightarrow t \subseteq s) $$$
Lean4
theorem mem_nhdsSet (hU : IsOpen s) : s ∈ 𝓝ˢ t ↔ t ⊆ s := by rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]