eventually_nhdsWithin_of_eventually_nhds

English

If p holds eventually in the usual neighborhood of a, then it holds eventually in the nhdsWithin neighborhood 𝓝[s] a.

Русский

Если p выполняется вплоть до предела в обычной окрестности a, то она выполняется в окрестности nhdsWithin a относительно s.

LaTeX

$$$ (∀ᶠ x \in 𝓝 a, p x) \rightarrow (∀ᶠ x \in 𝓝[s] a, p x) $$$

Lean4

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

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