cexp

Mathlib.Analysis.SpecialFunctions.Exp

URI: https://scilib.ai/kg/mathlib#ContinuousOn.cexp

English

For any set s, exp restricted to s is continuous on s.

Русский

Для произвольного множества s экспонтента ограничена на s непрерывна на s.

LaTeX

$$$$ \\operatorname{ContinuousOn}(\\exp, s). $$$$

Lean4

@[fun_prop]
theorem «cexp» (h : ContinuousOn f s) : ContinuousOn (fun y => exp (f y)) s := fun x hx => (h x hx).cexp

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

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

Разделы

Аффилиация

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