Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bounded_continuous_function.to_Lp_inj

Modification history

2023-01-08 13:02
src/measure_theory/function/lp_space.lean
feat(analysis/fourier): convergence of Fourier series (#17913) …
Added bounded_continuous_function.to_Lp_injView on Github →