setToFun_toL1 — Mathlib

English

If f is integrable, then setToFun μ T hT (f) = (toL1 f) mapped via the L1 representation equals the same setToFun value as above.

Русский

При интегрируемости f, значение setToFun равно соответствующему L1-образу f.

LaTeX

$$$\mathrm{setToFun}(\mu, T)\,h_T\,f = \mathrm{setToFun}(\mu, T)\,h_T\, (\text{toL1}(f))$$$

Lean4

theorem setToFun_toL1 (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) :
    setToFun μ T hT (hf.toL1 f) = setToFun μ T hT f :=
  setToFun_congr_ae hT hf.coeFn_toL1

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