map_exp_nhds

Mathlib.Analysis.SpecialFunctions.Exp

URI: https://scilib.ai/kg/mathlib#Real.map_exp_nhds

English

For each x, map exp of nhds x equals nhds of exp x.

Русский

Для каждой точки x отображение экспоненты переводит окрестности в окрестности эксп(x).

LaTeX

$$$\\mathrm{map}(\\exp, \\mathcal{N}_{x}) = \\mathcal{N}_{e^{x}}.$$$

Lean4

@[simp]
theorem map_exp_nhds (x : ℝ) : map exp (𝓝 x) = 𝓝 (exp x) :=
  isOpenEmbedding_exp.map_nhds_eq x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru