eventually_nhdsWithin_iff — Mathlib

English

If a predicate p holds eventually near a in the full neighborhood 𝓝 a, then it also holds eventually near a in the restricted neighborhood 𝓝[s] a.

Русский

Если свойство p выполняется почти что в окрестности a, то в окрестности внутри s это свойство тоже выполняется вплоть до пределa.

LaTeX

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

Lean4

theorem eventually_nhdsWithin_iff {a : α} {s : Set α} {p : α → Prop} :
    (∀ᶠ x in 𝓝[s] a, p x) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → p x :=
  eventually_inf_principal

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