Def ContinuousMap.sigmaCodHomeomorph

Modification history

2023-07-11 08:59
Mathlib/Topology/ContinuousFunction/Sigma.lean
feat: homeomorphism between `C(X, Σ i, Y i)` and `Σ i, C(X, Y i)` (#5673) …
Added ContinuousMap.sigmaCodHomeomorphView on Github →