integral_eq_integral — Mathlib

English

Let f be an L1-simple function f : α →₁ₛ[μ] E. Then its Bochner integral equals the integral of its simple-function representative: ∫ f dμ = ∫ (toSimpleFunc f) dμ.

Русский

Пусть f — простая функция в пространстве L1, f : α →₁ₛ[μ] E. Тогда интеграл Бо́чнера от f равен интегралу по μ от соответствующей простой функции: ∫ f dμ = ∫ (toSimpleFunc f) dμ.

LaTeX

$$$\int f \, d\mu = \int \big(\mathrm{toSimpleFunc} \, f\big) \, d\mu$$$

Lean4

theorem integral_eq_integral (f : α →₁ₛ[μ] E) : integral f = (toSimpleFunc f).integral μ :=
  rfl

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