English
Let f be an almost everywhere equal class of functions from α to ε with respect to μ. The statement defines Integrable(f) by the integrability of any (hence every) representative function; in other words, an AEEqFun-valued function is integrable exactly when a representative function is μ-integrable.
Русский
Пусть f -- класс функций по эквивалентности почти везде на α относительно μ. При этом интегрируемость определяется как интегрируемость любого представителя; то есть элемент в AEEqFun инвариантен в отношении μ и интегрируем тогда, когда любой представитель интегрируем по μ.
LaTeX
$$$\text{Integrable}(f) \;\equiv\; \mathrm{MeasureTheory}.\mathrm{Integrable} (f, \mu)$$$
Lean4
/-- A class of almost everywhere equal functions is `Integrable` if its function representative
is integrable. -/
def Integrable (f : α →ₘ[μ] ε) : Prop :=
MeasureTheory.Integrable f μ
