OAI/Geometry/Cannon/CirclePacking/Det.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonPackingGeometry.cyclic_folded_frames_positions line 13
  2. theorem OAI.CannonPackingGeometry.cyclic_fan_global_frame line 67
  3. lemma OAI.CannonPackingGeometry.sum_range_partition line 102
  4. lemma OAI.CannonPackingGeometry.polar_nonnegative_arg line 113
  5. theorem OAI.CannonPackingGeometry.closed_fan_cones_cover line 123
  6. def OAI.CannonTangentWedges.det line 157
  7. lemma OAI.CannonTangentWedges.barycentric line 159
  8. lemma OAI.CannonTangentWedges.combination_norm_sq line 166
  9. theorem OAI.CannonTangentWedges.wedge_ball_opposite_positive line 172
  10. lemma OAI.CannonPackingGeometry.orientedArea_eq_det line 214
  11. lemma OAI.CannonPackingGeometry.orientedArea_cyclic line 218
  12. lemma OAI.CannonPackingGeometry.orientedArea_swap_first line 220
  13. lemma OAI.CannonPackingGeometry.winding_area_eq line 222
  14. def OAI.CannonPackingGeometry.TriInterior line 225
  15. lemma OAI.CannonPackingGeometry.TriInterior.isometry line 230
  16. lemma OAI.CannonPackingGeometry.TriInterior.of_positive line 234
  17. lemma OAI.CannonPackingGeometry.TriInterior.inside line 240
  18. lemma OAI.CannonPackingGeometry.TriInterior.edge_positive line 249
  19. lemma OAI.CannonPackingGeometry.TriInterior.of_vertices line 268
  20. lemma OAI.CannonPackingGeometry.isometry_area_ne_zero line 275
  21. theorem OAI.CannonPackingGeometry.finite_star_ball_cover line 291