OAI/Geometry/PlaneColoring/Palettes.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EuclideanFiveColor.Traces line 9
  2. def OAI.EuclideanFiveColor.tracePositive line 10
  3. lemma OAI.EuclideanFiveColor.tracePositive_measurable line 12
  4. def OAI.EuclideanFiveColor.paletteGenerators line 15
  5. lemma OAI.EuclideanFiveColor.paletteGenerators_countable line 17
  6. def OAI.EuclideanFiveColor.paletteSet line 19
  7. lemma OAI.EuclideanFiveColor.paletteSet_measurable line 21
  8. lemma OAI.EuclideanFiveColor.tracePositive_le_palette line 23
  9. lemma OAI.EuclideanFiveColor.paletteSet_minimal line 26
  10. def OAI.EuclideanFiveColor.palette line 35
  11. lemma OAI.EuclideanFiveColor.mem_palette line 38
  12. lemma OAI.EuclideanFiveColor.palette_nonempty line 40
  13. lemma OAI.EuclideanFiveColor.inner_oneL2_integral line 63
  14. lemma OAI.EuclideanFiveColor.sample_inner_one line 68
  15. lemma OAI.EuclideanFiveColor.transition_avoiding_trace line 72
  16. lemma OAI.EuclideanFiveColor.edge_palette_not_pair line 103