English
If T and T' are pointwise equal on all measurable s with finite μ-measure, then for every f, setToFun μ T hT f = setToFun μ T' hT' f.
Русский
Если T и T' равны по всем измеримым множествам s с конечной мерой, то для любого f выполняется равенство SetToFun.
LaTeX
$$$\forall s, \text{MeasurableSet}(s) \Rightarrow \mu s < \infty \Rightarrow T s = T' s \Rightarrow setToFun\, μ\, T\, h_T\, f = setToFun\, μ\, T'\, h_T'\, f$$$
Lean4
theorem setToFun_congr_left' (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
(h : ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s) (f : α → E) : setToFun μ T hT f = setToFun μ T' hT' f :=
by
by_cases hf : Integrable f μ
· simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left' T T' hT hT' h]
· simp_rw [setToFun_undef _ hf]
