integral_id

Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

English

Let a, b be real numbers. Then ∫_a^b x dx equals (b^2 − a^2)/2.

Русский

Пусть a, b — действительные числа. Тогда ∫_a^b x dx = (b^2 − a^2)/2.

LaTeX

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

Lean4

@[simp]
theorem integral_id : ∫ x in a..b, x = (b ^ 2 - a ^ 2) / 2 :=
  by
  have := @integral_pow a b 1
  norm_num at this
  exact this

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

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

Разделы

Аффилиация

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