map_nhds_induced_of_mem — Mathlib

English

If range f is in the neighborhood filter of f(a), then map f (nhds a) = nhds (f a).

Русский

Если range f содержится в окрестностном фильтре f(a), то map f (nhds a) = nhds (f a).

LaTeX

$$$\\text{If } range\\ f \\in 𝓝 (f a),\\; \\operatorname{map} f (\\mathcal{N}_{\\mathrm{induced}\\ f}(a)) = \\mathcal{N}(f a).$$$

Lean4

theorem map_nhds_induced_of_mem {a : α} (h : range f ∈ 𝓝 (f a)) : map f (@nhds α (induced f t) a) = 𝓝 (f a) := by
  rw [nhds_induced, Filter.map_comap_of_mem h]

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