integrable_coeFn — Mathlib

English

For a function f in the AEEqFun space, the integrability of its cast representative is equivalent to the integrability of f itself: Integrable f.cast μ ↔ Integrable f.

Русский

Для f в пространстве AEEqFun интегрируемость представителя f.cast по μ эквивалентна интегрируемости самого f.

LaTeX

$$$\mathrm{Integrable}(f.cast, \mu) \;\iff\; \mathrm{Integrable}(f)$$$

Lean4

theorem integrable_coeFn {f : α →ₘ[μ] ε} : MeasureTheory.Integrable f μ ↔ Integrable f := by
  rw [← integrable_mk f.aestronglyMeasurable, mk_coeFn]

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