integral_congr — Mathlib

English

If f and g are L1-simple functions and they agree almost everywhere after applying toSimpleFunc, then their integrals are equal: if toSimpleFunc f =ᵐ[μ] toSimpleFunc g, then ∫ f = ∫ g.

Русский

Если две простые функции L1 совпадают почти повсеместно после применения toSimpleFunc, то их интегралы совпадают: если toSimpleFunc f =ᵐ[μ] toSimpleFunc g, то ∫ f = ∫ g.

LaTeX

$$$\text{toSimpleFunc } f =_{\mu}\!\!\! toSimpleFunc g \Rightarrow \int f = \int g$$$

Lean4

nonrec theorem integral_congr {f g : α →₁ₛ[μ] E} (h : toSimpleFunc f =ᵐ[μ] toSimpleFunc g) : integral f = integral g :=
  SimpleFunc.integral_congr (SimpleFunc.integrable f) h

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