English
In a T1 space, the set of points x for which x has the property that eventually p holds in nhdsWithin x with the complement of x is open.
Русский
В T1-пространстве множество точек x, для которых истинно свойство, что относительно окрестностей x с учетом дополнения к {x} выполняется, является открытым.
LaTeX
$$$\\forall X [\\mathcal{T}_1(X)], \\{x : X \\mid (\\forall^\\infty y \\text{ in } nhdsWithin(x, X\\setminus\\{x\\}), p(y))\\} \\text{ открыто.}$$$
Lean4
theorem isOpen_setOf_eventually_nhdsWithin [T1Space X] {p : X → Prop} : IsOpen {x | ∀ᶠ y in 𝓝[≠] x, p y} :=
by
refine isOpen_iff_mem_nhds.mpr fun a ha => ?_
filter_upwards [eventually_nhds_nhdsWithin.mpr ha] with b hb
rcases eq_or_ne a b with rfl | h
· exact hb
· rw [h.symm.nhdsWithin_compl_singleton] at hb
exact hb.filter_mono nhdsWithin_le_nhds
