English
If f1=f1' a.e. and f2=f2' a.e., then for any g: β→γ→ℝ≥0∞, the lintegral of g(f1,f2) equals the lintegral of g(f1',f2').
Русский
Если f1 = f1' a.e. и f2 = f2' a.e., тогда для любой g: β→γ→ℝ≥0∞ выполняется равенство линеграла g(f1,f2) и g(f1',f2').
LaTeX
$$$$ (f_1 =_{\\mathrm{ae}} f_1') \\land (f_2 =_{\\mathrm{ae}} f_2') \\Rightarrow \\forall g: β \\to γ \\to \\mathbb{R}_{\\ge 0}^{\\infty}, \\\\int^- a: \\alpha \\to \\mathbb{R}_{\\ge 0}^{\\infty}, g(f_1(a), f_2(a)) \\, d\\mu = \\int^- a, g(f_1'(a), f_2'(a)) \\, d\\mu. $$$$
Lean4
theorem lintegral_rw₂ {f₁ f₁' : α → β} {f₂ f₂' : α → γ} (h₁ : f₁ =ᵐ[μ] f₁') (h₂ : f₂ =ᵐ[μ] f₂') (g : β → γ → ℝ≥0∞) :
∫⁻ a, g (f₁ a) (f₂ a) ∂μ = ∫⁻ a, g (f₁' a) (f₂' a) ∂μ :=
lintegral_congr_ae <| h₁.mp <| h₂.mono fun _ h₂ h₁ => by dsimp only; rw [h₁, h₂]
