setIntegral_piecewise — Mathlib

English

The integral of g over piecewise hs κ η at a equals the piecewise-defined integral using κ or η depending on whether a ∈ s.

Русский

Интеграл по piecewise hs κ η в точке a равен соответствующему интегралу, который выбирается по условию a ∈ s.

LaTeX

$$$\\int g \\, d(\\mathrm{piecewise}(hs, κ, η)) (a) = \\begin{cases} \\int g \\, dκ(a) & \\text{если } a \\in s \\\\ \\int g \\, dη(a) & \\text{если } a \\notin s \\end{cases}$$$

Lean4

theorem setIntegral_piecewise (a : α) (g : β → E) (t : Set β) :
    ∫ b in t, g b ∂piecewise hs κ η a = if a ∈ s then ∫ b in t, g b ∂κ a else ∫ b in t, g b ∂η a := by
  simp_rw [piecewise_apply]; split_ifs <;> rfl

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