lintegral_add_measure — Mathlib

English

For f: α → ℝ≥0∞, and measures μ, ν, ∫ f d(μ+ν) = ∫ f dμ + ∫ f dν.

Русский

Для f и мер μ, ν: ∫ f d(μ+ν) = ∫ f dμ + ∫ f dν.

LaTeX

$$$\\int f \\, d(\\mu + \\nu) = \\int f \\, d\\mu + \\int f \\, d\\nu$$$

Lean4

@[simp]
theorem lintegral_add_measure (f : α → ℝ≥0∞) (μ ν : Measure α) : ∫⁻ a, f a ∂(μ + ν) = ∫⁻ a, f a ∂μ + ∫⁻ a, f a ∂ν :=
  by
  simp only [lintegral, SimpleFunc.lintegral_add, iSup_subtype']
  refine (ENNReal.iSup_add_iSup ?_).symm
  rintro ⟨φ, hφ⟩ ⟨ψ, hψ⟩
  refine ⟨⟨φ ⊔ ψ, sup_le hφ hψ⟩, ?_⟩
  gcongr
  exacts [le_sup_left, le_sup_right]

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