eventually_nhds_nhdsWithin — Mathlib

English

A two-step eventuality equivalence: eventual at nhdsWithin a s of y leads to eventual at nhdsWithin a s of x.

Русский

Утверждение о предельной частоте двух шагов в nhdsWithin: из будущего при y следует будущее при a.

LaTeX

$$Iff (Filter.Eventually (fun y => Filter.Eventually (fun x => p x) (nhdsWithin y s)) (nhdsWithin a s))$$

Lean4

@[simp]
theorem eventually_nhds_nhdsWithin {a : α} {s : Set α} {p : α → Prop} :
    (∀ᶠ y in 𝓝 a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x :=
  Filter.ext_iff.1 nhds_bind_nhdsWithin {x | p x}

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