integral_zero — Mathlib

English

The integral of the zero function is zero, by simplification.

Русский

Интеграл нулевой функции равен нулю; следует из определения.

LaTeX

$$$\\int _\\alpha 0 \\, d\\mu = 0$$$

Lean4

@[simp]
theorem integral_zero : ∫ _ : α, (0 : G) ∂μ = 0 :=
  by
  by_cases hG : CompleteSpace G
  · simp only [integral, hG, L1.integral]
    exact setToFun_zero (dominatedFinMeasAdditive_weightedSMul μ)
  · simp [integral, hG]

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