integral_const_of_cdf — Mathlib

English

If f is almost everywhere equal to 0 on Ioc a b, then its interval integral is 0.

Русский

Если f равно нулю почти всюду на Ioc(a,b), то интеграл по интервалу равен 0.

LaTeX

$$$ \\text{If } f = 0 \\,\\text{a.e. on } Ioc(a,b), \\text{ then } \\int_{a}^{b} f(x) \\, dμ = 0.$$$

Lean4

/-- If `μ` is a finite measure then `∫ x in a..b, c ∂μ = (μ (Iic b) - μ (Iic a)) • c`. -/
theorem integral_const_of_cdf [CompleteSpace E] [IsFiniteMeasure μ] (c : E) :
    ∫ _ in a..b, c ∂μ = (μ.real (Iic b) - μ.real (Iic a)) • c :=
  by
  simp only [sub_smul, ← setIntegral_const]
  refine (integral_Iic_sub_Iic ?_ ?_).symm <;> simp

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