English
For any sets s, t in a T1 space, the inclusion of their neighborhood-set filters corresponds to subset inclusion: 𝓝ˢ(s) ≤ 𝓝ˢ(t) if and only if s ⊆ t.
Русский
Для любых множеств s, t в T1-пространстве включение фильтров окрестностей множества соответствует включению множеств: 𝓝ˢ(s) ≤ 𝓝ˢ(t) тогда и только тогда, когда s ⊆ t.
LaTeX
$$$\mathcal{N}_{\mathrm{nhds}}(s) \leq \mathcal{N}_{\mathrm{nhds}}(t) \;\iff\; s \subseteq t$$$
Lean4
@[simp]
theorem nhdsSet_le_iff [T1Space X] {s t : Set X} : 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t :=
by
refine ⟨?_, fun h => monotone_nhdsSet h⟩
simp_rw [Filter.le_def]; intro h x hx
specialize h { x }ᶜ
simp_rw [compl_singleton_mem_nhdsSet_iff] at h
by_contra hxt
exact h hxt hx
