integral_const_on_unit_interval

Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

English

For any a and any real b, the integral of the constant b over [a, a+1] equals b.

Русский

Для любых a и вещественного b интеграл константы b по [a, a+1] равен b.

LaTeX

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

Lean4

theorem integral_const_on_unit_interval : ∫ _ in a..a + 1, b = b := by simp

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

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

Разделы

Аффилиация

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