English
For every x in the source and predicate p on Y, the eventual property in nhdsWithin e.symm⁻¹ s of e x is equivalent to the eventual property in nhdsWithin x of s applied to x.
Русский
Для каждого x в источнике и для предиката p на Y, свойство в nhdsWithin согласуется с nhdsWithin x относительно множества s.
LaTeX
$$$\\forall x: X, p:\\, Y \\to \\mathrm{Prop}, (e: OpenPartialHomeomorph X Y) \\;: \\ (\\forall^* y \\in \\mathcal{N}_{\\symm}^{s}(e(x)), p(y)) \\iff (\\forall^* x \\in \\mathcal{N}^{s}(x), p(e(x))).$$$
Lean4
theorem eventually_nhdsWithin {x : X} (p : Y → Prop) {s : Set X} (hx : x ∈ e.source) :
(∀ᶠ y in 𝓝[e.symm ⁻¹' s] e x, p y) ↔ ∀ᶠ x in 𝓝[s] x, p (e x) :=
by
refine Iff.trans ?_ eventually_map
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]
