integral_of_isEmpty — Mathlib

English

For an empty index type, the integral of any function is zero: ∫ f dμ = 0 when α is empty.

Русский

Для пустого множества индексов интеграл любой функции равен нулю: ∫ f dμ = 0 при пустом пространстве α.

LaTeX

$$$$\int x, f(x) \partial\mu = 0.$$$$

Lean4

theorem integral_of_isEmpty [IsEmpty α] {f : α → G} : ∫ x, f x ∂μ = 0 :=
  μ.eq_zero_of_isEmpty ▸ integral_zero_measure _

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