Commit 2023-07-11 08:59 51c2f54c

View on Github →

feat: homeomorphism between C(X, Σ i, Y i) and Σ i, C(X, Y i) (#5673) This is a follow-up to #4325.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Constructions.lean

added theorem inducing_sigma

Modified Mathlib/Topology/ContinuousFunction/Basic.lean

added def ContinuousMap.sigmaMk

Created Mathlib/Topology/ContinuousFunction/Sigma.lean

added theorem ContinuousMap.embedding_sigmaMk_comp

added theorem ContinuousMap.exists_lift_sigma

added def ContinuousMap.sigmaCodHomeomorph