lintegral_congr — Mathlib

English

If μ(f^{-1}({y})) = ν(g^{-1}({y})) for all y, then f.lintegral μ = g.lintegral ν.

Русский

Если для всех y верны равенства μ(f^{-1}({y})) = ν(g^{-1}({y})), то f.lintegral μ = g.lintegral ν.

LaTeX

$$$\\forall y, μ(f^{-1}({y})) = ν(g^{-1}({y})) \\Rightarrow f.lintegral μ = g.lintegral ν$$$

Lean4

/-- If two simple functions are equal a.e., then their `lintegral`s are equal. -/
theorem lintegral_congr {f g : α →ₛ ℝ≥0∞} (h : f =ᵐ[μ] g) : f.lintegral μ = g.lintegral μ :=
  lintegral_eq_of_measure_preimage fun y => measure_congr <| Eventually.set_eq <| h.mono fun x hx => by simp [hx]

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