OAI/Combinatorics/EuclideanRamsey/PathFractions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanRamsey.RightFraction line 31
  2. def OAI.EuclideanRamsey.HasDiagonal line 34
  3. def OAI.EuclideanRamsey.PairInverse line 36
  4. lemma OAI.EuclideanRamsey.RightFraction.one line 40
  5. lemma OAI.EuclideanRamsey.RightFraction.inv line 43
  6. lemma OAI.EuclideanRamsey.RightFraction.conjugate line 48
  7. lemma OAI.EuclideanRamsey.conjugate_single line 57
  8. lemma OAI.EuclideanRamsey.RightFraction.mul_single line 62
  9. def OAI.EuclideanRamsey.singleFractions line 78
  10. instance OAI.EuclideanRamsey.singleFractions_normal line 90
  11. lemma OAI.EuclideanRamsey.RightFraction.mul_pair line 97
  12. structure OAI.EuclideanRamsey.GradedPaths line 124
  13. def OAI.EuclideanRamsey.GradedPaths.monoid line 130
  14. lemma OAI.EuclideanRamsey.GradedPaths.diagonal line 135
  15. def OAI.EuclideanRamsey.GradedPaths.BoundedFraction line 137
  16. lemma OAI.EuclideanRamsey.GradedPaths.bounded_exists line 140
  17. lemma OAI.EuclideanRamsey.GradedPaths.bounded_fraction line 145
  18. lemma OAI.EuclideanRamsey.GradedPaths.bounded_one line 150
  19. lemma OAI.EuclideanRamsey.GradedPaths.bounded_mono line 153
  20. lemma OAI.EuclideanRamsey.GradedPaths.bounded_inv line 158
  21. lemma OAI.EuclideanRamsey.GradedPaths.bounded_conjugate line 163
  22. lemma OAI.EuclideanRamsey.GradedPaths.bounded_mul_single line 170
  23. def OAI.EuclideanRamsey.GradedPaths.singleCost line 186
  24. lemma OAI.EuclideanRamsey.GradedPaths.singleCost_bounded line 187
  25. lemma OAI.EuclideanRamsey.GradedPaths.singleCost_le line 190
  26. lemma OAI.EuclideanRamsey.GradedPaths.singleCost_one line 192
  27. lemma OAI.EuclideanRamsey.GradedPaths.singleCost_inv line 196
  28. lemma OAI.EuclideanRamsey.GradedPaths.singleCost_conjugate line 205
  29. lemma OAI.EuclideanRamsey.GradedPaths.singleCost_mul line 215
  30. lemma OAI.EuclideanRamsey.GradedPaths.bounded_tuple_list line 222