OAI/Geometry/PlaneColoring/Coloring.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.ProperColoring line 7

    Distinct definitions of this name: ComparatorChallenges/EuclideanFiveColor.lean:7 (different declaration text). Qualify references as OAI.EuclideanFiveColor.ProperColoring@path.

  2. instance OAI.EuclideanFiveColor.anglePeriodPositive line 15
  3. abbrev OAI.EuclideanFiveColor.Angles line 16
  4. def OAI.EuclideanFiveColor.angularMeasure line 17
  5. def OAI.EuclideanFiveColor.direction line 18
  6. instance OAI.EuclideanFiveColor.(instance at line 19) line 19
  7. instance OAI.EuclideanFiveColor.(instance at line 20) line 20
  8. lemma OAI.EuclideanFiveColor.direction_continuous line 21
  9. lemma OAI.EuclideanFiveColor.direction_norm line 22
  10. lemma OAI.EuclideanFiveColor.direction_real line 23
  11. def OAI.EuclideanFiveColor.WeakColoring line 27

    Source documentation

    Exactly the manuscript weak measurable condition, using normalized Haar angular measure. A function is understood up to a plane-null set; no regularity is imposed on a proper coloring.

    def WeakColoring (k : ℕ) (c : ℂ → Fin k) : Prop :=
…