eventually_nhds — Mathlib

English

There is an equivalence between eventual properties in the image neighborhood and the original neighborhood via e.

Русский

Свойства, удовлетворяющиеся по крайней мере часто в окрестности образа, эквивалентны соответствующим свойствам в исходной окрестности через e.

LaTeX

$$$(\\forall p: Y \\to \\mathrm{Prop}), (\\forall^* y \\in \\mathcal{N}(e(x)), p(y)) \\iff (\\forall^* x \\in \\mathcal{N}(x), p(e(x)))$$$

Lean4

theorem eventually_nhds {x : X} (p : Y → Prop) (hx : x ∈ e.source) : (∀ᶠ y in 𝓝 (e x), p y) ↔ ∀ᶠ x in 𝓝 x, p (e x) :=
  Iff.trans (by rw [e.map_nhds_eq hx]) eventually_map

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