abs_integral_eq_abs_integral_uIoc

English

For a real-valued f, the absolute value of the integral over [a,b] equals the absolute value of the integral over Ι a b: |∫_{a}^{b} f x dμ| = |∫_{Ι a b} f x dμ|.

Русский

Для вещественно-значной функции f: ℝ → ℝ справедливо |∫_{a}^{b} f(x) dx| = |∫_{Ι a b} f(x) dx|.

LaTeX

$$$\left|\int_{a}^{b} f(x) \, d\mu\right| = \left|\int_{Ι a b} f(x) \, d\mu\right|$$$

Lean4

theorem abs_integral_eq_abs_integral_uIoc (f : ℝ → ℝ) : |∫ x in a..b, f x ∂μ| = |∫ x in Ι a b, f x ∂μ| :=
  norm_integral_eq_norm_integral_uIoc f

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