of_finite — Mathlib

English

If S is a finite subset of α and μ is finite, then for any f: α → E, f is μ-integrable on S.

Русский

Если S — конечное подмножество α и μ — конечная мера, то для любой f: α → E функция f интегрируема по μ на S.

LaTeX

$$$\forall f:\alpha\to E,\forall S\subseteq \alpha,\ |S|<\infty\Rightarrow \int_{S} \|f(x)\| \, d\mu(x) < \infty$$$

Lean4

theorem of_finite [MeasurableSingletonClass α] {μ : Measure α} [IsFiniteMeasure μ] {s : Set α} (hs : s.Finite)
    {f : α → E} : IntegrableOn f s μ := by simpa using IntegrableOn.finset (s := hs.toFinset)

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