eventually_nhdsSet_iff_forall — Mathlib

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

Похожие утверждения