integral_one

Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

English

For any a, b ∈ ℝ, the integral of the constant function 1 over [a, b] equals b − a.

Русский

Для любых a, b ∈ ℝ интеграл от константы 1 по отрезку [a, b] равен b − a.

LaTeX

$$$\forall a,b \in \mathbb{R},\ \displaystyle \int_a^b 1 \, dx = b - a$$$

Lean4

theorem integral_one : (∫ _ in a..b, (1 : ℝ)) = b - a := by simp only [mul_one, smul_eq_mul, integral_const]

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

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

Разделы

Аффилиация

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