Commit 2026-01-13 20:29 e15dc82c
View on Github →feat(MeasureTheory): every bounded continuous function is in L∞ (#33776)
As opposed to the lemma right below we use MemLp and not f.toContinuousMap.toAEEqFun μ ∈ Lp, because
the later seems rather unergonomic and with MemLp it is possible to obtain a Lp function using MemLp.toLp.