OAI/CategoryTheory/Thomason/GraySquares.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Gray Squares.

  1. abbrev OAI.Thomason.GrayComposition.G line 15
  2. abbrev OAI.Thomason.GrayComposition.T line 16
  3. abbrev OAI.Thomason.GrayComposition.face line 17
  4. abbrev OAI.Thomason.GrayComposition.tensorFace line 18
  5. abbrev OAI.Thomason.GrayComposition.endpoint line 19
  6. abbrev OAI.Thomason.GrayComposition.projection line 20
  7. lemma OAI.Thomason.GrayComposition.endpoint_natural line 22
  8. lemma OAI.Thomason.GrayComposition.projection_natural line 25
  9. abbrev OAI.Thomason.GrayComposition.P line 29
  10. abbrev OAI.Thomason.GrayComposition.Q line 31
  11. abbrev OAI.Thomason.GrayComposition.i₀ line 32
  12. abbrev OAI.Thomason.GrayComposition.i₁ line 33
  13. abbrev OAI.Thomason.GrayComposition.j₀ line 34
  14. abbrev OAI.Thomason.GrayComposition.j₁ line 35
  15. def OAI.Thomason.GrayComposition.cutEndpoint line 37
  16. def OAI.Thomason.GrayComposition.cutProjection line 42
  17. lemma OAI.Thomason.GrayComposition.face_top line 48
  18. lemma OAI.Thomason.GrayComposition.top_composable line 53
  19. def OAI.Thomason.GrayComposition.compositeCell line 64
  20. lemma OAI.Thomason.GrayComposition.compositeCell_bounded line 67
  21. def OAI.Thomason.GrayComposition.composition line 79
  22. def OAI.Thomason.GrayComposition.CooperationExists line 82
  23. def OAI.Thomason.GrayComposition.FirstMixedCooperation line 87
  24. structure OAI.Thomason.GrayTwo.Coordinates line 99
  25. def OAI.Thomason.GrayTwo.Coordinates.IsValid line 107
  26. abbrev OAI.Thomason.GrayTwo.K line 132
  27. def OAI.Thomason.GrayTwo.coordinates line 134
  28. lemma OAI.Thomason.GrayTwo.row_above line 144
  29. lemma OAI.Thomason.GrayTwo.bounded line 155
  30. lemma OAI.Thomason.GrayTwo.coordinates_valid line 158
  31. lemma OAI.Thomason.GrayTwo.coordinates_injective line 272
  32. def OAI.Thomason.GrayTwo.Coordinates.lower line 341
  33. def OAI.Thomason.GrayTwo.Coordinates.top line 345
  34. def OAI.Thomason.GrayTwo.Coordinates.row line 351
  35. lemma OAI.Thomason.GrayTwo.Coordinates.row_above line 362
  36. lemma OAI.Thomason.GrayTwo.Coordinates.row_positive line 366
  37. lemma OAI.Thomason.GrayTwo.Coordinates.row_boundary line 396
  38. def OAI.Thomason.GrayTwo.Coordinates.table line 464
  39. lemma OAI.Thomason.GrayTwo.Coordinates.coordinates_table line 474
  40. lemma OAI.Thomason.GrayTwo.table_coordinates line 484
  41. def OAI.Thomason.GrayTwo.coordinatesEquiv line 489
  42. def OAI.Thomason.GrayTwo.code line 506
  43. lemma OAI.Thomason.GrayTwo.code_valid line 624
  44. lemma OAI.Thomason.GrayTwo.forall_fin4 line 629
  45. lemma OAI.Thomason.GrayTwo.forall_fin6 line 636
  46. lemma OAI.Thomason.GrayTwo.vec_val_five line 644
  47. lemma OAI.Thomason.GrayTwo.vertex_0 line 657
  48. lemma OAI.Thomason.GrayTwo.vertex_1 line 666
  49. lemma OAI.Thomason.GrayTwo.vertex_2 line 675
  50. lemma OAI.Thomason.GrayTwo.vertex_3 line 684