eventually_nhdsWithin' — Mathlib

English

A variant of eventual nhdsWithin involving e and its left inverse.

Русский

Вариант eventual nhdsWithin с участием e и её левого обращения.

LaTeX

$$$(\\forall x: X)(p: X \\to \\mathrm{Prop}), (hx: x \\in \\mathrm{source}(e)) \;: \\ (\\forall^* y \\in \\mathcal{N}_{e^{-1}(s)}(x), p(e^{-1}(y))) \\iff \\forall^* x \\in \\mathcal{N}_{s}(x), p(x)$$$

Lean4

theorem eventually_nhdsWithin' {x : X} (p : X → Prop) {s : Set X} (hx : x ∈ e.source) :
    (∀ᶠ y in 𝓝[e.symm ⁻¹' s] e x, p (e.symm y)) ↔ ∀ᶠ x in 𝓝[s] x, p x :=
  by
  rw [e.eventually_nhdsWithin _ hx]
  refine
    eventually_congr <| (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_
  rw [hy]

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