integral_congr — Mathlib

English

If f and g are equal almost everywhere and both integrable, then their Bochner integrals are equal.

Русский

Если f и g равны почти всюду и оба интегрируемы, то их интегралы Бо́хнера равны.

LaTeX

$$$$ \\text{If } f =_{μ} g \\text{ and } f,g \\text{ integrable}, \\quad f_{\\\\text{integral}} μ = g_{\\\\text{integral}} μ. $$$$

Lean4

theorem integral_congr {f g : α →ₛ E} (hf : Integrable f μ) (h : f =ᵐ[μ] g) : f.integral μ = g.integral μ :=
  setToSimpleFunc_congr (weightedSMul μ) (fun _ _ => weightedSMul_null) weightedSMul_union hf h

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