of_subsingleton — Mathlib

English

Let α be a type with at most one element and μ a finite measure on α. Then for every function f: α → β (where β is a normed additive commutative group), f is integrable with respect to μ.

Русский

Пусть α — тип с не более чем одним элементом и μ — конечная мера на α. Тогда для любой функции f: α → β (где β — нормированная абелева группа) функция интегрируема по μ.

LaTeX

$$$\\text{If } Subsingleton(\\alpha) \\text{ and } μ(α) < \\infty, \\text{ then } ∀ f: α \\to β,\\; \\int_α \\|f(x)\\| \\, dμ < \\infty.$$$

Lean4

/-- This lemma is a special case of `Integrable.of_finite`. -/
theorem of_subsingleton [Subsingleton α] [IsFiniteMeasure μ] {f : α → β} : Integrable f μ :=
  .of_finite

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