integral_const — Mathlib

English

For constant c, ∫ c dμ = μ.real univ • c.

Русский

Для константы c интеграл равен μ.real univ умножить на c.

LaTeX

$$$\\\\int x \\, c \\, d\\\\mu = μ.real univ \\\\cdot c$$$

Lean4

@[simp]
theorem integral_const (c : E) : ∫ _ : α, c ∂μ = μ.real univ • c :=
  by
  by_cases hμ : IsFiniteMeasure μ
  · simp only [integral, hE, L1.integral]
    exact setToFun_const (dominatedFinMeasAdditive_weightedSMul _) _
  by_cases hc : c = 0
  · simp [hc, integral_zero]
  ·
    simp [measureReal_def, (integrable_const_iff_isFiniteMeasure hc).not.2 hμ, integral_undef,
      MeasureTheory.not_isFiniteMeasure_iff.mp hμ]

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