setToFun_measure_zero — Mathlib

English

If f equals g almost everywhere, then setToFun μ T hT f = setToFun μ T hT g.

Русский

Если функции равны почти повсеместно, то их изображения через setToFun совпадают.

LaTeX

$$$\forall f,g,\; f =_{\mathrm{ae}, \mu} g \Rightarrow \mathrm{setToFun}(\mu, T)\,h_T\,f = \mathrm{setToFun}(\mu, T)\,h_T\,g$$$

Lean4

theorem setToFun_measure_zero (hT : DominatedFinMeasAdditive μ T C) (h : μ = 0) : setToFun μ T hT f = 0 :=
  by
  have : f =ᵐ[μ] 0 := by simp [h, EventuallyEq]
  rw [setToFun_congr_ae hT this, setToFun_zero]

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