lintegral_add — Mathlib

English

For f,g ∈ α →ₘ[μ] ℝ≥0∞, the lintegral is additive: lintegral(f+g) = lintegral f + lintegral g.

Русский

Для f,g ∈ α →ₘ[μ] ℝ≥0∞ линтеграл сумм равен сумме лин интегралов.

LaTeX

$$lintegral_add (f g : α →ₘ[μ] ℝ≥0∞) : lintegral (f + g) = lintegral f + lintegral g$$

Lean4

theorem lintegral_add (f g : α →ₘ[μ] ℝ≥0∞) : lintegral (f + g) = lintegral f + lintegral g :=
  induction_on₂ f g fun f hf g _ => by simp [lintegral_add_left' hf.aemeasurable]

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