Commit 2025-06-03 12:54 883359d2
View on Github →feat(Topology/RestrictedProduct): continuity of maps from finite product of restricted product (#25349)
Generalize continuous_dom_prod to finitary products. To help, add some other lemmas relating the topology of restricted products to pi types.
From FLT.