Commit 2026-06-27 13:04 0f320b07
View on Github →feat(Topology/MetricSpace): the L^p direct sum of metric spaces (#40212)
Endow the direct sum ι →₀ X of ι-many copies of a metric space X with the L^p metric for any 1 ≤ p < ∞.
p = ∞ is theoretically possible too but currently annoying due to defects in our tactics/WithTop API. I am leaving it as future work.
Zulip