Commit 2023-07-22 20:51 560eeb2b

View on Github →

feat: the additive circle is path connected (#6022)

Estimated changes

Modified Mathlib/Analysis/Convex/Normed.lean

Modified Mathlib/Data/Set/Image.lean

added theorem Set.Quotient.range_mk''

Modified Mathlib/GroupTheory/Coset.lean

added theorem QuotientGroup.range_mk

Modified Mathlib/Topology/Connected.lean

added theorem Function.Surjective.connectedSpace

added theorem connectedSpace_iff_univ

added theorem preconnectedSpace_iff_univ

Modified Mathlib/Topology/Instances/AddCircle.lean

Modified Mathlib/Topology/PathConnected.lean

added theorem Function.Surjective.pathConnectedSpace

added theorem isPathConnected_range

added theorem isPathConnected_univ