lintegral_eq_of_measure_preimage — Mathlib

English

If two simple functions are equal almost everywhere, their lintegrals are equal.

Русский

Если две простые функции равны почти везде, их линеграль равны.

LaTeX

$${f =ᵃᵉ μ g} → f.lintegral μ = g.lintegral μ$$

Lean4

/-- `SimpleFunc.lintegral` depends only on the measures of `f ⁻¹' {y}`. -/
theorem lintegral_eq_of_measure_preimage [MeasurableSpace β] {f : α →ₛ ℝ≥0∞} {g : β →ₛ ℝ≥0∞} {ν : Measure β}
    (H : ∀ y, μ (f ⁻¹' { y }) = ν (g ⁻¹' { y })) : f.lintegral μ = g.lintegral ν :=
  by
  simp only [lintegral, ← H]
  apply lintegral_eq_of_subset
  simp only [H]
  intros
  exact mem_range_of_measure_ne_zero ‹_›

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