OAI/Geometry/PlaneColoring/FiveSupport.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.palette_neighbor_real line 9
  2. lemma OAI.EuclideanFiveColor.palette_neighbor_disjoint line 23
  3. def OAI.EuclideanFiveColor.stateSupport line 39
  4. lemma OAI.EuclideanFiveColor.ae_mem_stateSupport line 40
  5. lemma OAI.EuclideanFiveColor.ae_state_support line 44
  6. lemma OAI.EuclideanFiveColor.stateSupport_cover line 49
  7. lemma OAI.EuclideanFiveColor.stateSupport_shift_relation line 55
  8. lemma OAI.EuclideanFiveColor.stateSupport_nonempty_measure line 71
  9. def OAI.EuclideanFiveColor.fiveRealState line 82
  10. def OAI.EuclideanFiveColor.fiveSupport line 83
  11. lemma OAI.EuclideanFiveColor.five_realState_measurable line 84
  12. lemma OAI.EuclideanFiveColor.five_support_trace line 86
  13. lemma OAI.EuclideanFiveColor.five_support_step_ban line 90
  14. lemma OAI.EuclideanFiveColor.five_support_cover line 122
  15. lemma OAI.EuclideanFiveColor.five_support_next line 124
  16. lemma OAI.EuclideanFiveColor.five_support_prev line 128
  17. lemma OAI.EuclideanFiveColor.five_support_no_sixty line 138
  18. def OAI.EuclideanFiveColor.FiveComb.Adj line 152

    Source comment

    Independent finite arithmetic facts; the source labels are Z/5Z, represented by Fin 5.
    def Adj (i j : Fin 5) : Prop := i+1=j ∨ j+1=i
  19. instance OAI.EuclideanFiveColor.FiveComb.(instance at line 153) line 153
  20. lemma OAI.EuclideanFiveColor.FiveComb.contact_neighbors line 154
  21. lemma OAI.EuclideanFiveColor.FiveComb.opposite_contacts line 156
  22. lemma OAI.EuclideanFiveColor.FiveComb.adjacent_oriented line 158
  23. lemma OAI.EuclideanFiveColor.FiveComb.neighbors line 159
  24. lemma OAI.EuclideanFiveColor.FiveComb.two_bans line 160
  25. def OAI.EuclideanFiveColor.fiveSupportList line 170
  26. lemma OAI.EuclideanFiveColor.mem_fiveSupportList line 173
  27. lemma OAI.EuclideanFiveColor.five_contact_next line 175
  28. lemma OAI.EuclideanFiveColor.five_contact_prev line 185
  29. lemma OAI.EuclideanFiveColor.five_opposite_contacts_false line 199
  30. lemma OAI.EuclideanFiveColor.plane_lipschitz_image_null line 241
  31. lemma OAI.EuclideanFiveColor.palette_open_exclusion line 247
  32. lemma OAI.EuclideanFiveColor.transitionEdge_no_open_exclusion line 301
  33. lemma OAI.EuclideanFiveColor.finite_closed_family_locally_subset line 342
  34. lemma OAI.EuclideanFiveColor.finite_closed_family_no_common_limit line 351
  35. lemma OAI.EuclideanFiveColor.stateSupport_local_pred line 365