toLargerSpace — Mathlib

English

If two measurable functions are almost everywhere equal, their integrals are equal.

Русский

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

LaTeX

$$$\\int f \\, d\\mu = \\int g \\, d\\mu$ if $f =_{\\mu\\text{-a.e.}} g$$$

Lean4

/-- Simple function seen as simple function of a larger `MeasurableSpace`. -/
def toLargerSpace (hm : m ≤ m0) (f : @SimpleFunc β m γ) : SimpleFunc β γ :=
  ⟨@SimpleFunc.toFun β m γ f, fun x => hm _ (@SimpleFunc.measurableSet_fiber β γ m f x),
    @SimpleFunc.finite_range β γ m f⟩

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