Commit 2024-04-16 07:44 38a7a533

View on Github →

feat(Analysis/SpecialFunctions/Complex/Circle): expMapCircle as a PartialHomeomorph and prove IsLocalHomeomorph (#11334) This PR proves IsLocalHomeomorph expMapCircle (eventually this should be upgraded to IsCoveringMap, but that's a good deal harder and is probably best done via general theory such as in #7596).

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

added theorem AddCircle.homeomorphCircle'_apply_mk

added theorem AddCircle.homeomorphCircle_apply

added theorem AddCircle.toCircle_apply_mk

added theorem isLocalHomeomorph_expMapCircle

Modified Mathlib/Topology/Instances/AddCircle.lean

added def AddCircle.homeomorphAddCircle

added theorem AddCircle.homeomorphAddCircle_apply_mk

added theorem AddCircle.homeomorphAddCircle_symm_apply_mk

added theorem AddCircle.isLocalHomeomorph_coe

added def AddCircle.partialHomeomorphCoe