Theorem lp.memℓp_of_tendsto

Modification history

2023-09-19 04:03
Mathlib/Analysis/NormedSpace/lpSpace.lean
refactor(Topology/MetricSpace): remove `Metric.Bounded` (#7240) …
Modified lp.memℓp_of_tendstoView on Github →
2023-06-01 05:16
Mathlib/Analysis/NormedSpace/LpSpace.lean
feat: port Analysis.NormedSpace.LpSpace (#4465) …
Added lp.memℓp_of_tendstoView on Github →