integral_Iic_add_Ioi — Mathlib

English

A rearrangement identity for interval integrals: ∫_a^b f = ∫_a^d + ∫_d^b with appropriate adjustments.

Русский

Существуют перестановочные соотношения для интегралов по интервалам: разложение по разбиению [a,b] через точку d.

LaTeX

$$$ \\int_{a}^{b} f(x) \\, dμ = \\int_{a}^{d} f(x) \\, dμ + \\int_{d}^{b} f(x) \\, dμ $$$

Lean4

theorem integral_Iic_add_Ioi (h_left : IntegrableOn f (Iic b) μ) (h_right : IntegrableOn f (Ioi b) μ) :
    (∫ x in Iic b, f x ∂μ) + (∫ x in Ioi b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ :=
  by
  convert (setIntegral_union (Iic_disjoint_Ioi <| Eq.le rfl) measurableSet_Ioi h_left h_right).symm
  rw [Iic_union_Ioi, Measure.restrict_univ]

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