OAI/Geometry/PlaneColoring/States.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.fourGroup line 8
  2. def OAI.EuclideanFiveColor.fourEdge line 9
  3. def OAI.EuclideanFiveColor.fourCanonical line 11
  4. def OAI.EuclideanFiveColor.FourAdmissible line 12
  5. lemma OAI.EuclideanFiveColor.fourGroup_nonempty line 14
  6. lemma OAI.EuclideanFiveColor.four_admissible_group line 16
  7. lemma OAI.EuclideanFiveColor.four_group_unique line 19
  8. lemma OAI.EuclideanFiveColor.four_admissible_character line 21
  9. lemma OAI.EuclideanFiveColor.four_trace_edge line 29
  10. lemma OAI.EuclideanFiveColor.LineDensityZero.mono_ae line 39
  11. def OAI.EuclideanFiveColor.DensityZero line 49
  12. lemma OAI.EuclideanFiveColor.DensityZero.mono line 52
  13. lemma OAI.EuclideanFiveColor.DensityZero.union line 57
  14. lemma OAI.EuclideanFiveColor.densityZero_empty line 66
  15. lemma OAI.EuclideanFiveColor.DensityZero.biUnion_finset line 69
  16. lemma OAI.EuclideanFiveColor.DensityZero.compl line 78
  17. def OAI.EuclideanFiveColor.RealState line 92
  18. lemma OAI.EuclideanFiveColor.state_densityZero line 94
  19. lemma OAI.EuclideanFiveColor.angularSum_swap line 102
  20. lemma OAI.EuclideanFiveColor.states_densityOne line 106
  21. lemma OAI.EuclideanFiveColor.DensityOne.compl line 130
  22. lemma OAI.EuclideanFiveColor.DensityOne.inter line 143
  23. lemma OAI.EuclideanFiveColor.DensityOne.measure_ne_zero line 147
  24. lemma OAI.EuclideanFiveColor.densityOne_univ line 155
  25. lemma OAI.EuclideanFiveColor.DensityOne.iInter line 161
  26. lemma OAI.EuclideanFiveColor.finite_density_realization line 173
  27. lemma OAI.EuclideanFiveColor.two_label_triangle_impossible line 198
  28. lemma OAI.EuclideanFiveColor.bool_flip_two line 217
  29. lemma OAI.EuclideanFiveColor.bool_flip_three line 223
  30. lemma OAI.EuclideanFiveColor.bool_flip_even line 228
  31. lemma OAI.EuclideanFiveColor.triangleAngle_nonparallel line 240
  32. lemma OAI.EuclideanFiveColor.two_state_impossible line 243
  33. def OAI.EuclideanFiveColor.FourCenter line 315
  34. lemma OAI.EuclideanFiveColor.four_palette_admissible line 317
  35. def OAI.EuclideanFiveColor.fourState line 325
  36. lemma OAI.EuclideanFiveColor.fourState_measurable line 326
  37. lemma OAI.EuclideanFiveColor.fourState_group line 330
  38. lemma OAI.EuclideanFiveColor.fourState_represents line 333
  39. lemma OAI.EuclideanFiveColor.fourState_changes line 341
  40. lemma OAI.EuclideanFiveColor.three_exclude_flip line 349
  41. lemma OAI.EuclideanFiveColor.fourState_diagonal_positive line 351
  42. lemma OAI.EuclideanFiveColor.varying_pullback_L1 line 389
  43. lemma OAI.EuclideanFiveColor.indicator_inter_positive line 415
  44. lemma OAI.EuclideanFiveColor.circleEndpoint_identity_neighborhood line 449
  45. lemma OAI.EuclideanFiveColor.near_identity_circle_in line 465
  46. lemma OAI.EuclideanFiveColor.nonparallel_neighborhood line 527
  47. lemma OAI.EuclideanFiveColor.strict_state_sequence_local_false line 547
  48. lemma OAI.EuclideanFiveColor.positive_state_support_point line 642
  49. lemma OAI.EuclideanFiveColor.support_density_direction line 664
  50. lemma OAI.EuclideanFiveColor.support_density_sequence line 672
  51. lemma OAI.EuclideanFiveColor.strict_state_sequence_false line 683
  52. lemma OAI.EuclideanFiveColor.strict_state_no_unit_support line 704
  53. lemma OAI.EuclideanFiveColor.complex_unit_orthogonal line 726
  54. lemma OAI.EuclideanFiveColor.ae_direction_nonorthogonal line 752