OAI/Geometry/Cannon/CirclePacking/PetalAngle.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonPackingGeometry.petalAngle line 14
  2. lemma OAI.CannonPackingGeometry.petalAngle_zero_left line 16
  3. lemma OAI.CannonPackingGeometry.petalAngle_zero_right line 18
  4. lemma OAI.CannonPackingGeometry.petalAngle_continuous line 21
  5. def OAI.CannonPackingGeometry.RingData line 25
  6. lemma OAI.CannonPackingGeometry.interval_constant line 33
  7. theorem OAI.CannonPackingGeometry.RingData.first_pos line 40
  8. lemma OAI.CannonPackingGeometry.ringData_closed line 102
  9. lemma OAI.CannonPackingGeometry.ringData_compact line 122
  10. theorem OAI.CannonPackingGeometry.exists_ring_constant line 131
  11. lemma OAI.CannonPackingGeometry.RingData.pos line 151
  12. theorem OAI.CannonPackingGeometry.exists_bounded_ring_constant line 206
  13. lemma OAI.CannonPackingGeometry.radius_fraction_mem line 240
  14. lemma OAI.CannonPackingGeometry.tangent_petal_angle line 243
  15. lemma OAI.CannonPackingGeometry.fanRay_dist_sq_pair line 262
  16. lemma OAI.CannonPackingGeometry.tangent_nonoverlap_cosine line 276
  17. theorem OAI.CannonPackingGeometry.actual_fan_ringData line 288