OAI/Geometry/CylinderCovering/Angular/Margins.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.Cubic.profile_le_max_endpoints line 10
  2. theorem OAI.CylinderCovering.Cubic.profile_bounds line 30
  3. theorem OAI.CylinderCovering.Cubic.coeff_bounds line 37
  4. theorem OAI.CylinderCovering.Cubic.profile_nonneg line 51
  5. theorem OAI.CylinderCovering.Cubic.profileMax_nonneg line 55
  6. theorem OAI.CylinderCovering.Cubic.cap_pos line 58
  7. theorem OAI.CylinderCovering.Cubic.shared_left line 63
  8. theorem OAI.CylinderCovering.Cubic.shared_right line 66
  9. theorem OAI.CylinderCovering.Cubic.beta_error line 69
  10. theorem OAI.CylinderCovering.Cubic.alpha_error line 75
  11. theorem OAI.CylinderCovering.Cubic.first_crossing line 91
  12. theorem OAI.CylinderCovering.Cubic.step_pos line 106
  13. theorem OAI.CylinderCovering.Cubic.node_zero line 110
  14. theorem OAI.CylinderCovering.Cubic.node_last line 112
  15. theorem OAI.CylinderCovering.Cubic.node_succ line 118
  16. theorem OAI.CylinderCovering.Cubic.node_abs_le line 122
  17. theorem OAI.CylinderCovering.Cubic.angular_sector line 136
  18. theorem OAI.CylinderCovering.Cubic.angle_in_interval line 167
  19. theorem OAI.CylinderCovering.Cubic.abs_le_of_interval line 171
  20. theorem OAI.CylinderCovering.Cubic.ceil_count_pos line 175
  21. theorem OAI.CylinderCovering.Cubic.ceil_step_le line 179
  22. theorem OAI.CylinderCovering.Cubic.selected_cuts line 186
  23. theorem OAI.CylinderCovering.Cubic.finite_coordinate_cover line 245
  24. theorem OAI.CylinderCovering.Cubic.finite_coordinate_cover_ceil line 267