OAI/Geometry/PlaneColoring/PaletteTransport.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.angleRep_preserving line 8
  2. lemma OAI.EuclideanFiveColor.weak_lift_Ioc line 12
  3. lemma OAI.EuclideanFiveColor.weak_restrict line 37
  4. lemma OAI.EuclideanFiveColor.weak_lift_set line 52
  5. lemma OAI.EuclideanFiveColor.weak_strong_disjoint_single line 67
  6. lemma OAI.EuclideanFiveColor.weak_strong_disjoint_single_eventual line 118
  7. lemma OAI.EuclideanFiveColor.palette_trace_branch line 145
  8. lemma OAI.EuclideanFiveColor.palette_branch_local line 210
  9. lemma OAI.EuclideanFiveColor.circleInverse_left line 236
  10. lemma OAI.EuclideanFiveColor.circleEndpoint_eventuallyEq line 241
  11. lemma OAI.EuclideanFiveColor.ae_of_locally_ae line 258
  12. lemma OAI.EuclideanFiveColor.ae_restrict_of_locally_ae line 269
  13. lemma OAI.EuclideanFiveColor.palette_transport_real line 286
  14. lemma OAI.EuclideanFiveColor.endpoint_fiber_nonzero line 310
  15. lemma OAI.EuclideanFiveColor.palette_smooth_transport line 345
  16. lemma OAI.EuclideanFiveColor.palette_transport_param line 362
  17. def OAI.EuclideanFiveColor.sixty line 390
  18. lemma OAI.EuclideanFiveColor.sin_sixty_ne line 391
  19. lemma OAI.EuclideanFiveColor.sin_twice_sixty_ne line 394
  20. lemma OAI.EuclideanFiveColor.sixty_sum line 397
  21. lemma OAI.EuclideanFiveColor.ae_angular_of_ae_line line 411
  22. lemma OAI.EuclideanFiveColor.ae_sin_sub_ne_zero line 419
  23. lemma OAI.EuclideanFiveColor.palette_sixty_real line 433
  24. lemma OAI.EuclideanFiveColor.palette_sixty line 444
  25. lemma OAI.EuclideanFiveColor.palette_sixty_disjoint line 450