map_nhds_of_mem — Mathlib

English

If f is inducing and range f ∈ 𝓝(f x), then (𝓝 x).map f = 𝓝(f x).

Русский

Если f индуцирующее и range f ∈ 𝓝(f(x)), то (𝓝 x).map f = 𝓝(f x).

LaTeX

$$$\operatorname{IsInducing}(f) \Rightarrow \forall x, \operatorname{range}(f) \in \mathcal{N}(f(x)) \Rightarrow (\mathcal{N}(x)).map f = \mathcal{N}(f(x)).$$$

Lean4

theorem map_nhds_of_mem (hf : IsInducing f) (x : X) (h : range f ∈ 𝓝 (f x)) : (𝓝 x).map f = 𝓝 (f x) :=
  hf.eq_induced ▸ map_nhds_induced_of_mem h

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