English
If for every measurable s with finite μ(s) we have T s x = T' s x for all x, then f.setToSimpleFunc T = f.setToSimpleFunc T' for any simple function f.
Русский
Если для каждого измеримого множества s с конечной мерой μ(s) выполняется T s x = T' s x для всех x, то для любой простой функции f выполняется равенство f.setToSimpleFunc T = f.setToSimpleFunc T'.
LaTeX
$$$(\forall s, MeasurableSet s, μ s < \infty) \Rightarrow T s x = T' s x \Rightarrow f.setToSimpleFunc T f = f.setToSimpleFunc T' f$$$
Lean4
theorem setToSimpleFunc_congr (T : Set α → E →L[ℝ] F) (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T) {f g : α →ₛ E} (hf : Integrable f μ) (h : f =ᵐ[μ] g) :
f.setToSimpleFunc T = g.setToSimpleFunc T :=
by
refine setToSimpleFunc_congr' T h_add hf ((integrable_congr h).mp hf) ?_
refine fun x y hxy => h_zero _ ((measurableSet_fiber f x).inter (measurableSet_fiber g y)) ?_
rw [EventuallyEq, ae_iff] at h
refine measure_mono_null (fun z => ?_) h
simp_rw [Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_preimage, Set.mem_singleton_iff]
intro h
rwa [h.1, h.2]
