Theorem MeasureTheory.MemLp.prodLp_fst

Modification history

2025-08-08 00:06
Mathlib/MeasureTheory/SpecificCodomains/WithLp.lean
feat: integrability in a product space (#27674) …
Added MeasureTheory.MemLp.prodLp_fstView on Github →