lintegral_of_isEmpty — Mathlib

English

If α is empty, then ∫ f dμ = 0 for any f: α → ℝ≥0∞.

Русский

Если множество пустое, то интеграл равен нулю для любой функции.

LaTeX

$$$\\int^⁻ a, f(a) \\partial μ = 0$$$

Lean4

@[simp]
theorem lintegral_of_isEmpty {α} [MeasurableSpace α] [IsEmpty α] (μ : Measure α) (f : α → ℝ≥0∞) : ∫⁻ x, f x ∂μ = 0 :=
  by
  have : Subsingleton (Measure α) := inferInstance
  convert lintegral_zero_measure f

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