English
(∀ᶠ x in nhdsSet s, p x) ↔ ∀ x, x ∈ s → ∀ᶠ y in nhds x, p y.
Русский
Если высказывание p выполняется достаточно часто в nhdsSet s, значит для каждого x ∈ s верно, что p достигается локально вокруг x.
LaTeX
$$$(\\forallᶠ x \\in nhdsSet s, p x) \\iff \\forall x, x \\in s \\rightarrow \\forallᶠ y \\in nhds x, p y$$$
Lean4
/-- A proposition is true on a set neighborhood of `s`
iff it is eventually true near each point in the set. -/
theorem eventually_nhdsSet_iff_forall {p : X → Prop} : (∀ᶠ x in 𝓝ˢ s, p x) ↔ ∀ x, x ∈ s → ∀ᶠ y in 𝓝 x, p y :=
mem_nhdsSet_iff_forall