isOpenMap_exp — Mathlib

English

The exponential map exp: C → C is an open mapping, i.e., it sends open sets to open sets.

Русский

Функция экспоненты exp: ℂ → ℂ является открытым отображением: образы открытых множеств открыты.

LaTeX

$$$$ \forall U \subseteq \mathbb{C},\quad U \text{ открыто } \Rightarrow \exp(U) \text{ открыто в } \mathbb{C}. $$$$

Lean4

theorem isOpenMap_exp : IsOpenMap exp :=
  isOpenMap_of_hasStrictDerivAt hasStrictDerivAt_exp exp_ne_zero

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