const_lintegral — Mathlib

English

The lintegral of a constant simple function equals the constant times the measure of the whole space.

Русский

Линеграль константной простой функции равен константе, умноженной на меру всего пространства.

LaTeX

$$$\\bigl(\\text{const } α\\, c\\bigr).lintegral μ = c \\cdot μ(\\mathrm{univ})$$$

Lean4

theorem const_lintegral (c : ℝ≥0∞) : (const α c).lintegral μ = c * μ univ :=
  by
  rw [lintegral]
  cases isEmpty_or_nonempty α
  · simp [μ.eq_zero_of_isEmpty]
  · simp only [range_const, coe_const, Finset.sum_singleton]
    unfold Function.const; rw [preimage_const_of_mem (mem_singleton c)]

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