lintegral_fintype — Mathlib

English

If α is finite, the lintegral equals the finite sum over α of f(x)μ({x}).

Русский

Если тип α конечен, линтеграл равен конечной сумме по всем x∈α f(x)μ({x}).

LaTeX

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

Lean4

theorem lintegral_fintype [MeasurableSingletonClass α] [Fintype α] (f : α → ℝ≥0∞) : ∫⁻ x, f x ∂μ = ∑ x, f x * μ { x } :=
  by rw [← lintegral_finset, Finset.coe_univ, Measure.restrict_univ]

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