integrableOn_exp_neg_Ioi

Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

URI: https://scilib.ai/kg/mathlib#integrableOn_exp_neg_Ioi

← MathLib Explorer

English

For any c, the function x -> exp(-x) is integrable on Ioi(c).

Русский

Для любого c функция x -> exp(-x) интегрируема на Ioi(c).

LaTeX

$$$$ \\int_{c}^{\\infty} e^{-x} dx < \\infty.$$$$

Lean4

theorem integrableOn_exp_neg_Ioi (c : ℝ) : IntegrableOn (fun (x : ℝ) => exp (-x)) (Ioi c) :=
  Iff.mp integrableOn_Ici_iff_integrableOn_Ioi (integrableOn_exp_Iic (-c)).comp_neg_Ici

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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