integral_cases — Mathlib

English

The norm of the interval integral equals the integral of the norm over the restricted interval.

Русский

Норма интервального интеграла равна интегралу нормы на ограниченном интервале.

LaTeX

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

Lean4

theorem integral_cases (f : ℝ → E) (a b) :
    (∫ x in a..b, f x ∂μ) ∈ ({∫ x in Ι a b, f x ∂μ, -∫ x in Ι a b, f x ∂μ} : Set E) := by
  rw [intervalIntegral_eq_integral_uIoc]; split_ifs <;> simp

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