integrable_mk — Mathlib

English

For a function f that is AEStronglyMeasurable, Integrable mk f hf is equivalent to MeasureTheory.Integrable f μ; i.e., integrability for the equivalence-class version corresponds to integrability of the representative function.

Русский

Пусть f полностью измерим и интегрируем; тогда интегрируемость эквивалентна интегрируемости представителя функции f по мереб μ.

LaTeX

$$$\text{Integrable}(\mathrm{mk}(f, hf)) \iff \mathrm{Integrable}(f, \mu)$$$

Lean4

theorem integrable_mk {f : α → ε} (hf : AEStronglyMeasurable f μ) :
    Integrable (mk f hf : α →ₘ[μ] ε) ↔ MeasureTheory.Integrable f μ :=
  by
  simp only [Integrable]
  apply integrable_congr
  exact coeFn_mk f hf

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