continuous_expMap — Mathlib

English

The map expMap is a continuous map from realSpace K to realSpace K, as a product map of continuous expMap_single components.

Русский

Отображение expMap непрерывно как произведение компонент expMap_single.

LaTeX

$$$\\mathrm{Continuous}(\\mathrm{expMap} : \\mathrm{realSpace} K \\to \\mathrm{realSpace} K)$$$

Lean4

theorem continuous_expMap : Continuous (expMap : realSpace K → realSpace K) :=
  continuousOn_univ.mp <| (expMap_source K) ▸ expMap.continuousOn

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