Theorems · Definition · general topology
Circle.centeredArc
ℝ → Set Circle
The image under Circle.exp of the interval of angles (-r, r).
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- Set.ofPredproof · cited by 6,101
- Set.imageproof · cited by 5,609
- absproof · cited by 1,814
- Circlestatement · cited by 227
- Circle.expproof · cited by 73
Cited by9
Results whose statement or proof uses this declaration.
- Circle.centeredArc_eq_emptystatement and proof · cited by 2
- Circle.mem_centeredArcstatement and proof · cited by 1
- Circle.mem_centeredArc_divstatement and proof · cited by 1
- Circle.hasBasis_centeredArc_div_two_powstatement and proof · cited by 1
- Circle.centeredArc_zerostatement · cited by 1
- Circle.isOpen_centeredArcstatement · cited by 0
- Circle.eq_one_of_forall_pow_mem_centeredArc_pi_div_twostatement and proof · cited by 0
- Circle.bijOn_exp_Ioo_centeredArcstatement · cited by 0
- Circle.centeredArc_monostatement and proof · cited by 0