Theorems · Definition · complex analysis
Complex.expOpenPartialHomeomorph
OpenPartialHomeomorph ℂ ℂ
Complex.exp as an OpenPartialHomeomorph with source = {z | -π < im z < π} and
target = {z | 0 < re z} ∪ {z | im z ≠ 0} (a.k.a. slitPlane).
This definition is used to prove that Complex.log
is complex differentiable at all points but the negative real semi-axis.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredproof · cited by 6,101
- Complexstatement and proof · cited by 5,565
- Real.piproof · cited by 1,774
- Set.Iooproof · cited by 1,214
- OpenPartialHomeomorphstatement · cited by 664
- Complex.expproof · cited by 612
- Complex.improof · cited by 591
- Complex.logproof · cited by 187
- Complex.slitPlaneproof · cited by 113
- Complex.isOpen_slitPlaneproof · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- Complex.hasStrictDerivAt_logproof · cited by 8
- Complex.contDiffAt_logproof · cited by 0
- Complex.expPartialHomeomorphproof · cited by 0