OAI/Geometry/PlaneColoring/FourTransport.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.circleSum_one_lipschitz_sumTransport line 9
  2. def OAI.EuclideanFiveColor.sumTransport line 24
  3. lemma OAI.EuclideanFiveColor.sumTransport_measurable line 26
  4. lemma OAI.EuclideanFiveColor.sumTransport_neighborhood line 29
  5. def OAI.EuclideanFiveColor.fourNonSingleton line 85
  6. lemma OAI.EuclideanFiveColor.four_complement_support line 86
  7. lemma OAI.EuclideanFiveColor.four_support_transport line 99
  8. lemma OAI.EuclideanFiveColor.four_support_transport_general line 132
  9. lemma OAI.EuclideanFiveColor.two_closed_shift_separated_not_cover line 166
  10. lemma OAI.EuclideanFiveColor.closed_gap line 175
  11. lemma OAI.EuclideanFiveColor.positive_normalized_increment_enters_gap line 191
  12. lemma OAI.EuclideanFiveColor.direction_sixty_unit_real line 204
  13. lemma OAI.EuclideanFiveColor.four_support_nonempty line 211
  14. lemma OAI.EuclideanFiveColor.four_support_no_sixty line 218
  15. lemma OAI.EuclideanFiveColor.four_support_union_proper line 224
  16. lemma OAI.EuclideanFiveColor.four_outside_support_state line 230
  17. lemma OAI.EuclideanFiveColor.four_gap_length line 241
  18. lemma OAI.EuclideanFiveColor.four_gap_exists line 257
  19. lemma OAI.EuclideanFiveColor.open_subset_closed_of_ae line 282
  20. lemma OAI.EuclideanFiveColor.four_gap_shift_subset line 290
  21. lemma OAI.EuclideanFiveColor.strict_increment_limit line 316
  22. def OAI.EuclideanFiveColor.transportVelocity line 340
  23. lemma OAI.EuclideanFiveColor.circleInverseDeriv_fst line 342
  24. lemma OAI.EuclideanFiveColor.sumTransport_increment_limit line 356
  25. lemma OAI.EuclideanFiveColor.sumTransport_tendsto line 384
  26. lemma OAI.EuclideanFiveColor.transportVelocity_neg line 392
  27. lemma OAI.EuclideanFiveColor.sumTransport_double_increment line 396
  28. lemma OAI.EuclideanFiveColor.ae_angular_nonparallel line 423
  29. lemma OAI.EuclideanFiveColor.transportVelocity_ne line 430
  30. lemma OAI.EuclideanFiveColor.exists_transportVelocity_lt line 440