integral_pow — Mathlib

English

Let a, b be real numbers and n a natural number. Then the definite integral ∫_a^b x^n dx equals (b^(n+1) − a^(n+1)) / (n+1).

Русский

Пусть a, b — вещественные числа, n ∈ ℕ. Тогда пределенный интеграл ∫_a^b x^n dx равен (b^(n+1) − a^(n+1)) / (n+1).

LaTeX

$$$\forall a,b \in \mathbb{R},\ (n \in \mathbb{N}) \Rightarrow \displaystyle \int_a^b x^n \, dx = \frac{b^{n+1} - a^{n+1}}{n+1}$$$

Lean4

@[simp]
theorem integral_pow : ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) := by
  simpa only [← Int.natCast_succ, zpow_natCast] using integral_zpow (Or.inl n.cast_nonneg)

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