`BookProof.ChapterPvmFibreInducedSystem.lpCongr_symm_proj` {μ ν : Measure X} (h : μ = ν) {E : Set X} (hE : MeasurableSet E) (f : Lp ℂ 2 ν) : (lpCongr h).symm (proj ν hE f) = proj μ

Initializing...

`BookProof.ChapterPvmFibreInducedSystem.lpCongr_symm_proj` {μ ν : Measure X} (h : μ = ν) {E : Set X} (hE : MeasurableSet E) (f : Lp ℂ 2 ν) : (lpCongr h).symm (proj ν hE f) = proj μ · Prove2Me