abs_intervalIntegral_eq — Mathlib

English

The absolute value of interval integral equals the absolute value of the corresponding interval integral over uIoc.

Русский

Модуль интервального интеграла равен модулю соответствующего интервального интеграла по uIoc.

LaTeX

$$$|\\int x in a..b f(x) \\partial\\mu| = |\\int x in Ι a b f(x) \\partial\\mu|$$$

Lean4

theorem abs_intervalIntegral_eq (f : ℝ → ℝ) (a b : ℝ) (μ : Measure ℝ) :
    |∫ x in a..b, f x ∂μ| = |∫ x in Ι a b, f x ∂μ| :=
  norm_intervalIntegral_eq f a b μ

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