comap_exp_nhds_exp — Mathlib

English

The preimage under exp of the neighborhood of exp x is exactly the neighborhood of x; exp is a local homeomorphism.

Русский

Предобраз экспоненты окрестности exp x равен окрестности x; экспонента локальный гамеморфизм.

LaTeX

$$$\\mathrm{comap}(\\exp, \\mathcal{N}_{\\exp x}) = \\mathcal{N}_{x}.$$$

Lean4

@[simp]
theorem comap_exp_nhds_exp (x : ℝ) : comap exp (𝓝 (exp x)) = 𝓝 x :=
  (isOpenEmbedding_exp.nhds_eq_comap x).symm

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