`BookProof.ChapterLpRestrictSplit.restrictEmbed_coeFn` {A : Set α} (hA : MeasurableSet A) (u : Lp ℂ 2 (mu.restrict A)) : (restrictEmbed hA u : α → ℂ) =ᵐ[mu] A.indicator (u : α → ℂ)

Initializing...

`BookProof.ChapterLpRestrictSplit.restrictEmbed_coeFn` {A : Set α} (hA : MeasurableSet A) (u : Lp ℂ 2 (mu.restrict A)) : (restrictEmbed hA u : α → ℂ) =ᵐ[mu] A.indicator (u : α → ℂ) · Prove2Me