English
Let X be a topological space, s ⊆ X and p a predicate on X. If p holds eventually for y in the set-neighborhood filter 𝓝ˢ s, then for almost every such y, p holds eventually in the neighborhood 𝓝 y of y.
Русский
Пусть X — топологическое пространство, s ⊆ X и p — утверждение на X. Если p выполняется почти для y в фильтре 𝓝ˢ s, то почти для почти каждого y в 𝓝ˢ s выполнится p в некоторой окрестности y, то есть ∀ᶠ x в 𝓝 y, p x.
LaTeX
$$$(\\forall p : X \\to \\mathsf{Prop})\\ (\\forall^\\infty y \\in \\mathcal{N}^\\mathsf{set}(s), p(y)) \\Rightarrow (\\forall^\\infty y \\in \\mathcal{N}^\\mathsf{set}(s), \\forall^\\infty x \\in \\mathcal{N}(y), p(x))$$$
Lean4
theorem eventually_nhdsSet {p : X → Prop} (h : ∀ᶠ y in 𝓝ˢ s, p y) : ∀ᶠ y in 𝓝ˢ s, ∀ᶠ x in 𝓝 y, p x :=
eventually_nhdsSet_iff_forall.mpr fun x x_in ↦ (eventually_nhdsSet_iff_forall.mp h x x_in).eventually_nhds
