Commit 2023-06-30 17:15 73c58c77

View on Github →

feat: lift a continuous map from a connected space to a sigma type (#4325) Motivated by a theorem in the Brouwer Fixed Point project

Estimated changes

Modified Mathlib/Data/Set/Image.lean

added theorem Set.range_subset_range_iff_exists_comp

Modified Mathlib/Data/Sigma/Basic.lean

added theorem Function.eq_of_sigmaMk_comp

Modified Mathlib/Topology/Connected.lean

added theorem Continuous.exists_lift_sigma