Mathlib Map

Theorems · Theorem · general topology

Circle.compl_range_path

∀ {x y : Circle}, x ≠ y → (Set.range ⇑(x.path y))ᶜ = ⇑(y.path x) '' Set.Ioo 0 1
Defined in
Mathlib.Analysis.SpecialFunctions.Complex.Circle
Cited by
1 results in Mathlib
Foundations
Depth 207 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.range_path_ssubset_univ · cited by 1Circle.range_path_ssubset…DFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetReal · cited by 25697RealSet.Elem · cited by 7166Set.ElemSet.image · cited by 5609Set.imageSet.range · cited by 4705Set.rangeCompl.compl · cited by 2925Compl.complSet.Ioo · cited by 1214Set.IooSet.Ioc · cited by 971Set.IocLT.lt.ne · cited by 872lt.neunitInterval · cited by 607unitIntervalPath · cited by 318PathCircle · cited by 227CircleComplex.arg · cited by 220Complex.argSet.union_singleton · cited by 107Set.union_singletonCircle.compl_range_pathCITED BYCITES

Cites30

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
  • Set.rangestatement · cited by 4,705
  • Compl.complstatement and proof · cited by 2,925
  • Set.Ioostatement and proof · cited by 1,214
  • Set.Iocproof · cited by 971
  • LT.lt.neproof · cited by 872
  • unitIntervalstatement and proof · cited by 607
  • Pathstatement · cited by 318

Cited by1

Results whose statement or proof uses this declaration.