setToFun_non_aestronglyMeasurable

English

If two sets of maps T and T' agree on all measurable sets of finite μ-measure, then setToFun μ T hT f equals setToFun μ T' hT' f for all f.

Русский

Если T и T' совпадают на всех измеримых множествах с конечной мерой, то setToFun μ T hT f = setToFun μ T' hT' f для всех f.

LaTeX

$$$T = T' \Rightarrow setToFun\, μ\, T\, h_T\, f = setToFun\, μ\, T'\, h_T'\, f$$$

Lean4

theorem setToFun_non_aestronglyMeasurable (hT : DominatedFinMeasAdditive μ T C) (hf : ¬AEStronglyMeasurable f μ) :
    setToFun μ T hT f = 0 :=
  setToFun_undef hT (not_and_of_not_left _ hf)

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