finset — Mathlib

English

Let μ be a finite measure on α and S a finite subset of α. For every function f: α → E, f is μ-integrable on S (i.e., ∫_S ∥f∥ dμ < ∞).

Русский

Пусть μ — конечная мера на α, и S — конечное подмножество α. Для любой функции f: α → E интегрируемость по μ на S: ∫_S ∥f∥ dμ < ∞.

LaTeX

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

Lean4

theorem finset [MeasurableSingletonClass α] {μ : Measure α} [IsFiniteMeasure μ] {s : Finset α} {f : α → E} :
    IntegrableOn f s μ := by
  rw [← s.toSet.biUnion_of_singleton]
  simp [integrableOn_finset_iUnion, measure_lt_top]

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