integral_exp_Iic — Mathlib

English

Let c be a real number. The improper integral of e^x over (-∞, c] equals e^c.

Русский

Пусть c ∈ ℝ. Непределённый интеграл по пределу от e^x на интервале (−∞, c] равен e^c.

LaTeX

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

Lean4

theorem integral_exp_Iic (c : ℝ) : ∫ x : ℝ in Iic c, exp x = exp c :=
  by
  refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Iic _ (integrableOn_exp_Iic _) tendsto_id) ?_
  simp_rw [integral_exp, show 𝓝 (exp c) = 𝓝 (exp c - 0) by rw [sub_zero]]
  exact tendsto_exp_atBot.const_sub _

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