setAverage_congr — Mathlib

English

If two sets s and t are almost everywhere equal, their restricted-averages agree: average_{μ|s} f = average_{μ|t} f.

Русский

Если множества s и t равны почти повсюду, их средние по ограниченным мерам совпадают.

LaTeX

$$$\operatorname{average}_{\mu|_s} f = \operatorname{average}_{\mu|_t} f \quad (s =_{a.e.,\mu} t)$$$

Lean4

theorem setAverage_congr (h : s =ᵐ[μ] t) : ⨍ x in s, f x ∂μ = ⨍ x in t, f x ∂μ := by
  simp only [setAverage_eq, setIntegral_congr_set h, measureReal_congr h]

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