Theorems · Definition · general topology
Circle.argPartialEquiv
PartialEquiv Circle ℝ
Complex.arg ∘ (↑) and Circle.exp define a partial equivalence between Circle and ℝ
with source = Set.univ and target = Set.Ioc (-π) π.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 198 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.
- DFunLike.coeproof · cited by 62,936
- Realstatement · cited by 25,697
- Set.univproof · cited by 3,945
- Real.piproof · cited by 1,774
- Set.Iocproof · cited by 971
- PartialEquivstatement · cited by 335
- Circlestatement and proof · cited by 227
- Complex.argproof · cited by 220
- Circle.expproof · cited by 73
- Circle.exp_argproof · cited by 6
Cited by7
Results whose statement or proof uses this declaration.
- Circle.argEquivproof · cited by 2
- Circle.invOn_arg_expproof · cited by 0
- Circle.surjOn_exp_neg_pi_piproof · cited by 0
- Circle.argPartialEquiv_applystatement and proof · cited by 0
- Circle.argPartialEquiv_sourcestatement and proof · cited by 0
- Circle.argPartialEquiv_symm_applystatement and proof · cited by 0
- Circle.argPartialEquiv_targetstatement and proof · cited by 0