integral_exp_Iic_zero

Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

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

English

For c = 0, the integral equals 1.

Русский

Пусть c = 0. Тогда неопр. интеграл по пределу от e^x на (-∞, 0] равен 1.

LaTeX

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

Lean4

theorem integral_exp_Iic_zero : ∫ x : ℝ in Iic 0, exp x = 1 :=
  exp_zero ▸ integral_exp_Iic 0

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

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

Разделы

Аффилиация

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