English
(∖forall) ∀ᶠ x in nhdsSet s, p x iff ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, p x.
Русский
Положено: существует открытое множество t, содержащее s, такое что ∀ x ∈ t, p x выполняется (производится eventually).
LaTeX
$$$(\\forallᶠ x \\in nhdsSet s, p x) \\iff \\exists t, IsOpen t ∧ s ⊆ t ∧ ∀ x, x ∈ t → p x$$$
Lean4
/-- A proposition is true on a set neighborhood of `s` iff it is true on a larger open set -/
theorem eventually_nhdsSet_iff_exists {p : X → Prop} : (∀ᶠ x in 𝓝ˢ s, p x) ↔ ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x, x ∈ t → p x :=
mem_nhdsSet_iff_exists