lintegral_finset — Mathlib

English

For a finite set s, the lintegral equals the finite sum over s of f(x)μ({x}) weighted by the point masses.

Русский

Для конечного множества s линтеграл равен конечной сумме по x∈s f(x)μ({x}).

LaTeX

$$$\int_{s} f(x) \, d\mu = \sum_{x \in s} f(x) \mu\{x\}$$$

Lean4

theorem lintegral_finset [MeasurableSingletonClass α] (s : Finset α) (f : α → ℝ≥0∞) :
    ∫⁻ x in s, f x ∂μ = ∑ x ∈ s, f x * μ { x } := by
  simp only [lintegral_countable _ s.countable_toSet, ← Finset.tsum_subtype']

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