norm_intervalIntegral_eq — Mathlib

English

The integral over a..b can be expressed using uIoc with a sign depending on a ≤ b.

Русский

Интеграл по a..b выражается через uIoc с знаком, зависящим от того, выполняется ли a ≤ b.

LaTeX

$$$(\\text{if } a \\le b) \\Rightarrow \\int x \\in a..b f(x) dx = \\int x \\in Ioc(a,b) f(x) dx;$$$

Lean4

theorem norm_intervalIntegral_eq (f : ℝ → E) (a b : ℝ) (μ : Measure ℝ) :
    ‖∫ x in a..b, f x ∂μ‖ = ‖∫ x in Ι a b, f x ∂μ‖ :=
  by
  simp_rw [intervalIntegral_eq_integral_uIoc, norm_smul]
  split_ifs <;> simp only [norm_neg, norm_one, one_mul]

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