English
If hT and hT' are dominated FinMeasAdditive with the same μ and if T = T', then setToL1 hT f = setToL1 hT' f for all f.
Русский
Если hT и hT' имеют одинаковую меру μ и T = T', то для любого f выполняется setToL1 hT f = setToL1 hT' f.
LaTeX
$$$hT = hT' \\Rightarrow \\forall f,\\; setToL1 hT f = setToL1 hT' f.$$$
Lean4
theorem setToL1_add_left (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
(f : α →₁[μ] E) : setToL1 (hT.add hT') f = setToL1 hT f + setToL1 hT' f :=
by
suffices setToL1 (hT.add hT') = setToL1 hT + setToL1 hT' by rw [this, ContinuousLinearMap.add_apply]
refine ContinuousLinearMap.extend_unique (setToL1SCLM α E μ (hT.add hT')) _ _ _ _ ?_
ext1 f
suffices setToL1 hT f + setToL1 hT' f = setToL1SCLM α E μ (hT.add hT') f by rw [← this]; simp [coeToLp]
rw [setToL1_eq_setToL1SCLM, setToL1_eq_setToL1SCLM, setToL1SCLM_add_left hT hT']
