setLAverage_congr — Mathlib

English

If sets s and t are almost everywhere equal with respect to μ, then the laverage of f with respect to μ.restrict s equals that with μ.restrict t.

Русский

Если s и t равны по μ-приближению, то laverage f по μ.s равен laverage f по μ.t.

LaTeX

$$$s =^{\\mathrm{ae}} t \\Rightarrow \\laverage_{\\mu\\restriction s}(f) = \\laverage_{\\mu\\restriction t}(f)$$$

Lean4

theorem setLAverage_congr (h : s =ᵐ[μ] t) : ⨍⁻ x in s, f x ∂μ = ⨍⁻ x in t, f x ∂μ := by
  simp only [setLAverage_eq, setLIntegral_congr h, measure_congr h]

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