setLIntegral_congr — Mathlib

English

If two sets s and t are μ-almost equal (s =ᵐ[μ] t), then the integrals of f over s and over t are equal: ∫_s f dμ = ∫_t f dμ.

Русский

Если множества s и t равны почти по μ, то интегралы по s и по t равны: ∫_s f dμ = ∫_t f dμ.

LaTeX

$$$\\int_s f \\, d\\mu = \\int_t f \\, d\\mu$$$

Lean4

theorem setLIntegral_congr {f : α → ℝ≥0∞} {s t : Set α} (h : s =ᵐ[μ] t) : ∫⁻ x in s, f x ∂μ = ∫⁻ x in t, f x ∂μ := by
  rw [Measure.restrict_congr_set h]

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