eventually_nhds' — Mathlib

English

A variant of the eventual nhds equivalence with a preimage under e.symm.

Русский

Вариант эквивалентности по eventually nhds с предобразом через e.symm.

LaTeX

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

Lean4

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

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