`BookProof.ChapterHilbertSumIntertwine.memLp_fibrewise` (B : ∀ i, G i →L[ℂ] G i) (hB : ∀ i u, ‖B i u‖ ≤ ‖u‖) (w : lp G 2) : Memℓp (fun i => B i (w i)) 2

Initializing...

`BookProof.ChapterHilbertSumIntertwine.memLp_fibrewise` (B : ∀ i, G i →L[ℂ] G i) (hB : ∀ i u, ‖B i u‖ ≤ ‖u‖) (w : lp G 2) : Memℓp (fun i => B i (w i)) 2 · Prove2Me