lintegral_rw₁ — Mathlib

English

If f and f' are equal almost everywhere with respect to μ, then for every function g, the lintegral of g∘f equals the lintegral of g∘f'.

Русский

Если f и f' равны почти повсюду по μ, тогда для всякой функции g выполняется равенство линегралов g(f) и g(f').

LaTeX

$$$$ (f =_{\\mathrm{ae}} f') \\Rightarrow \\forall g: \\beta \\to \\mathbb{R}_{\\ge 0}^{\\infty},\\\\\\int^- g(f) \\, d\\mu = \\int^- g(f') \\, d\\mu. $$$$

Lean4

theorem lintegral_rw₁ {f f' : α → β} (h : f =ᵐ[μ] f') (g : β → ℝ≥0∞) : ∫⁻ a, g (f a) ∂μ = ∫⁻ a, g (f' a) ∂μ :=
  lintegral_congr_ae <|
    h.mono fun a h => by dsimp only;
      rw [h]
        -- TODO: Need a better way of rewriting inside of an integral

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