Theorem bounded_continuous_function.coe_fn_to_Lp
Modification history
2023-01-08 13:02
src/measure_theory/function/lp_space.lean
feat(analysis/fourier): convergence of Fourier series (#17913) …
Modified bounded_continuous_function.coe_fn_to_LpView on Github →