integral_smul — Mathlib

English

The zero function is Integrable.

Русский

Нулевая функция интегрируема.

LaTeX

$$$\text{Integrable } I l (\lambda x. 0) vol$$$

Lean4

@[simp]
theorem integral_smul (c : ℝ) : integral I l (fun x => c • f x) vol = c • integral I l f vol :=
  by
  rcases eq_or_ne c 0 with (rfl | hc); · simp only [zero_smul, integral_zero]
  by_cases hf : Integrable I l f vol
  · exact (hf.hasIntegral.smul c).integral_eq
  · have : ¬Integrable I l (fun x => c • f x) vol := mt (fun h => h.of_smul hc) hf
    rw [integral, integral, dif_neg hf, dif_neg this, smul_zero]

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