OAI/Geometry/PlaneColoring/Accumulation.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.normalized_increment_endpoint_gap line 9
  2. lemma OAI.EuclideanFiveColor.four_support_positive line 20
  3. lemma OAI.EuclideanFiveColor.four_other_union line 26
  4. lemma OAI.EuclideanFiveColor.four_endpoint_sequence_false line 32
  5. lemma OAI.EuclideanFiveColor.gap_endpoint_nonorthogonal line 110
  6. lemma OAI.EuclideanFiveColor.triple_subset_pair line 129
  7. lemma OAI.EuclideanFiveColor.triangle_binary line 157
  8. lemma OAI.EuclideanFiveColor.triangle_centers_separated line 178
  9. lemma OAI.EuclideanFiveColor.transitionRatio_mono line 192
  10. lemma OAI.EuclideanFiveColor.transitionEdge_closed line 197
  11. lemma OAI.EuclideanFiveColor.missing_edge_lim line 214
  12. lemma OAI.EuclideanFiveColor.four_normalized_sequence_false line 233
  13. lemma OAI.EuclideanFiveColor.four_sequence_no_accumulation line 246
  14. lemma OAI.EuclideanFiveColor.fourCenter_closed line 270
  15. lemma OAI.EuclideanFiveColor.fourCenter_discrete line 273
  16. lemma OAI.EuclideanFiveColor.fourCenter_compact_finite line 281
  17. lemma OAI.EuclideanFiveColor.weak_relabel line 293
  18. lemma OAI.EuclideanFiveColor.transitionSet_relabel line 296
  19. lemma OAI.EuclideanFiveColor.transitionEdge_relabel line 300
  20. lemma OAI.EuclideanFiveColor.transitionEdge_symm line 307
  21. def OAI.EuclideanFiveColor.ThreeCenter line 324
  22. lemma OAI.EuclideanFiveColor.threeCenter_closed line 326
  23. lemma OAI.EuclideanFiveColor.three_sequence_no_accumulation line 329
  24. lemma OAI.EuclideanFiveColor.threeCenter_discrete line 339
  25. lemma OAI.EuclideanFiveColor.threeCenter_compact_finite line 348
  26. def OAI.EuclideanFiveColor.FiveCenter line 358
  27. lemma OAI.EuclideanFiveColor.five_palette_admissible line 359
  28. def OAI.EuclideanFiveColor.fiveState line 364
  29. lemma OAI.EuclideanFiveColor.palette_eq_measurable line 365
  30. lemma OAI.EuclideanFiveColor.fiveState_measurable line 373
  31. lemma OAI.EuclideanFiveColor.fiveState_diag line 378
  32. lemma OAI.EuclideanFiveColor.fiveState_represents line 381
  33. lemma OAI.EuclideanFiveColor.fiveState_adj line 390