of_subsingleton — Mathlib

English

If S is a subsingleton (contains at most one element) and μ is finite, then for every f: α → E, f is μ-integrable on S.

Русский

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

LaTeX

$$$\text{If } S\text{ is subsingleton and } μ\text{ is finite, then } \int_{S} \|f(x)\| \, d\mu(x) < \infty$$$

Lean4

theorem of_subsingleton [MeasurableSingletonClass α] {μ : Measure α} [IsFiniteMeasure μ] {s : Set α}
    (hs : s.Subsingleton) {f : α → E} : IntegrableOn f s μ :=
  .of_finite hs.finite

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