integral_exp_neg_Ioi_zero

Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

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

English

For c = 0, the integral of e^{-x} from 0 to ∞ equals 1.

Русский

Пусть c = 0. Тогда ∫_{0}^{∞} e^{-x} dx = 1.

LaTeX

$$$\\int_{0}^{\\infty} e^{-x} \\, dx = 1$$$

Lean4

theorem integral_exp_neg_Ioi_zero : (∫ x : ℝ in Ioi 0, exp (-x)) = 1 := by
  simpa only [neg_zero, exp_zero] using integral_exp_neg_Ioi 0

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

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

Разделы

Аффилиация

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