Mathlib Map

Theorems · Theorem · general topology

Circle.path_image_Ioc_of_ne

∀ {x y : Circle}, x ≠ y → ⇑(x.path y) '' Set.Ioc 0 1 = ⇑Circle.exp '' Set.Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
Defined in
Mathlib.Analysis.SpecialFunctions.Complex.Circle
Cited by
3 results in Mathlib
Foundations
Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Circle.disjoint_path_image_Ioc · cited by 2Circle.disjoint_path_imag…Circle.path_image_Ioc_union · cited by 1Circle.path_image_Ioc_uni…Circle.compl_range_path · cited by 1Circle.compl_range_pathDFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetReal · cited by 25697RealSet.Elem · cited by 7166Set.ElemSet.image · cited by 5609Set.imageComplex · cited by 5565ComplexSubmonoid · cited by 3086SubmonoidContinuousMap · cited by 2491ContinuousMapSet.Ioc · cited by 971Set.IocunitInterval · cited by 607unitIntervalPath · cited by 318PathCircle · cited by 227CircleComplex.arg · cited by 220Complex.argSet.image_comp · cited by 142Set.image_compSubmonoid.unitSphere · cited by 85Submonoid.unitSphereCircle.path_image_Ioc_of_neCITED BYCITES

Cites22

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • DFunLike.coestatement and proof · cited by 62,936
  • Setstatement and proof · cited by 53,352
  • Realstatement and proof · cited by 25,697
  • Set.Elemstatement and proof · cited by 7,166
  • Set.imagestatement and proof · cited by 5,609
  • Complexstatement · cited by 5,565
  • Submonoidstatement · cited by 3,086
  • ContinuousMapstatement · cited by 2,491
  • Set.Iocstatement and proof · cited by 971
  • unitIntervalstatement and proof · cited by 607
  • Pathstatement · cited by 318
  • Circlestatement and proof · cited by 227

Cited by3

Results whose statement or proof uses this declaration.