English
For a measurable set s with finite measure, the L1-setToL1 of the indicator constant function equals the value on s.
Русский
Для измеримой множества s с конечной мерой, L1-setToL1 индикаторной константы равно значению на s.
LaTeX
$$$setToL1 hT (simpleFunc.indicatorConst 1 hs hμs.ne x) = T s x$.$$
Lean4
theorem setToL1_congr_left (T T' : Set α → E →L[ℝ] F) {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C') (h : T = T') (f : α →₁[μ] E) : setToL1 hT f = setToL1 hT' f :=
by
suffices setToL1 hT = setToL1 hT' by rw [this]
refine ContinuousLinearMap.extend_unique (setToL1SCLM α E μ hT) _ _ _ _ ?_
ext1 f
suffices setToL1 hT' f = setToL1SCLM α E μ hT f by rw [← this]; simp [coeToLp]
rw [setToL1_eq_setToL1SCLM]
exact setToL1SCLM_congr_left hT' hT h.symm f
