continuous_exp

Mathlib.Analysis.SpecialFunctions.Exp

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

English

The real exponential function exp on ℝ is continuous.

Русский

Реальная экспонента exp на ℝ непрерывна.

LaTeX

$$$$ \\text{Continuous}(\\exp: \\mathbb{R} \\to \\mathbb{R}). $$$$

Lean4

@[continuity]
theorem continuous_exp : Continuous exp :=
  Complex.continuous_re.comp Complex.continuous_ofReal.cexp

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

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

Разделы

Аффилиация

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