eventually_nhdsWithin_of_forall — Mathlib

English

If p(x) holds for every x in s, then p(x) holds eventually at a with respect to nhdsWithin a s.

Русский

Если выполняется p(x) для каждого x из s, то p(x) выполняется периодически в окрестности a внутри s.

LaTeX

$$$ (\\forall x \\in s, p x) \\rightarrow \\forall^\\infty x \\in 𝓝[s] a, p x $$$

Lean4

theorem eventually_nhdsWithin_of_forall {s : Set α} {a : α} {p : α → Prop} (h : ∀ x ∈ s, p x) : ∀ᶠ x in 𝓝[s] a, p x :=
  mem_inf_of_right h

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