toSimpleFunc_eq_toFun — Mathlib

English

The toSimpleFunc of a Lp.simpleFunc has MemLp p μ.

Русский

toSimpleFunc(f) принадлежит MemLp p μ.

LaTeX

$$$\operatorname{MemLp}(\mathrm{toSimpleFunc}(f), p, \mu)$$$

Lean4

theorem toSimpleFunc_eq_toFun (f : Lp.simpleFunc E p μ) : toSimpleFunc f =ᵐ[μ] f :=
  show ⇑(toSimpleFunc f) =ᵐ[μ] ⇑(f : α →ₘ[μ] E)
    by
    convert (AEEqFun.coeFn_mk (toSimpleFunc f) (toSimpleFunc f).aestronglyMeasurable).symm using 2
    exact (Classical.choose_spec f.2).symm

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