map_nhds_eq — Mathlib

English

If f is open and continuous at x, then map f (nhds x) = nhds (f x).

Русский

Если f открытое и непрерывно в точке x, тогда применение к окрестности переносит её в окрестность изображения.

LaTeX

$$$$IsOpenMap(f) \\rightarrow \\forall x, ContinuousAt f x \\rightarrow map(f)(\\mathcal{N}(x)) = \\mathcal{N}(f(x))$$$$

Lean4

theorem map_nhds_eq (hf : IsOpenMap f) {x : X} (hf' : ContinuousAt f x) : map f (𝓝 x) = 𝓝 (f x) :=
  le_antisymm hf' (hf.nhds_le x)

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