exp_continuous — Mathlib

English

The exponential map is invertible for all x; exp(x) has a two-sided inverse given by exp(-x).

Русский

Экспонента инвертируема для любого x; обратный элемент exp(-x).

LaTeX

$$$\text{Exp invertible }\; (\forall x)\; (\exp 𝕂 x)^{-1} = \exp 𝕂 (-x)$$$

Lean4

@[continuity, fun_prop]
theorem exp_continuous : Continuous (exp 𝕂 : 𝔸 → 𝔸) :=
  by
  rw [← continuousOn_univ, ← Metric.eball_top_eq_univ (0 : 𝔸), ← expSeries_radius_eq_top 𝕂 𝔸]
  exact continuousOn_exp

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