OAI/Geometry/Cannon/CirclePacking/OrientedArea.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonPackingGeometry.orientedArea line 13
  2. theorem OAI.CannonPackingGeometry.normalize_edge line 15
  3. theorem OAI.CannonPackingGeometry.normalized_two_distances line 47
  4. theorem OAI.CannonPackingGeometry.congruent_triangle_isometry line 62
  5. theorem OAI.CannonPackingGeometry.point_unique_of_three_distances line 85
  6. theorem OAI.CannonPackingGeometry.triangle_isometry_unique line 110
  7. lemma OAI.CannonPackingGeometry.orientedArea_translate line 127
  8. lemma OAI.CannonPackingGeometry.orientedArea_rotate line 131
  9. lemma OAI.CannonPackingGeometry.orientedArea_conj line 139
  10. theorem OAI.CannonPackingGeometry.isometry_orientedArea_product line 144
  11. theorem OAI.CannonPackingGeometry.point_unique_of_two_distances_and_side line 162
  12. theorem OAI.CannonPackingGeometry.folded_edge_isometry line 181
  13. lemma OAI.CannonPackingGeometry.orientedArea_swap line 227
  14. theorem OAI.CannonPackingGeometry.folded_frames_compatible line 231
  15. theorem OAI.CannonPackingGeometry.positive_radii_triangle line 263
  16. lemma OAI.CannonPackingGeometry.orientedArea_ne_zero_of_strict line 309
  17. lemma OAI.CannonPackingGeometry.triangle_third_unique line 333
  18. theorem OAI.CannonPackingGeometry.triangle_chart line 346
  19. lemma OAI.CannonPackingGeometry.orientedArea_swap_edge line 371
  20. lemma OAI.CannonPackingGeometry.chart_area_ne_zero line 375
  21. def OAI.CannonPackingGeometry.Folds line 385
  22. lemma OAI.CannonPackingGeometry.Folds.swap line 390
  23. lemma OAI.CannonPackingGeometry.Folds.symm line 396
  24. theorem OAI.CannonPackingGeometry.exists_fold line 406
  25. def OAI.CannonPackingGeometry.fanRay line 438
  26. lemma OAI.CannonPackingGeometry.rotate_polar_dist line 440
  27. lemma OAI.CannonPackingGeometry.polar_distance_sq line 448
  28. lemma OAI.CannonPackingGeometry.polar_orientedArea line 456
  29. lemma OAI.CannonPackingGeometry.rotated_polar_orientedArea line 463
  30. lemma OAI.CannonPackingGeometry.fanRay_zero line 472
  31. lemma OAI.CannonPackingGeometry.fanRay_norm line 475
  32. lemma OAI.CannonPackingGeometry.fanRay_dist_sq line 478
  33. lemma OAI.CannonPackingGeometry.fanRay_orientedArea line 484
  34. theorem OAI.CannonPackingGeometry.closed_euclidean_fan line 489
  35. theorem OAI.CannonPackingGeometry.fan_triangle_frames line 510
  36. def OAI.CannonPackingGeometry.fanSucc line 535
  37. lemma OAI.CannonPackingGeometry.fanRay_succ line 538
  38. theorem OAI.CannonPackingGeometry.cyclic_folded_frames line 547
  39. theorem OAI.CannonPackingGeometry.finite_cyclic_folded_frames line 608