OAI/CategoryTheory/Globular/CutoffCells.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.GlobularSet.cutoffLow line 13
  2. def OAI.Grothendieck.GlobularSet.cutoffHigh line 16
  3. theorem OAI.Grothendieck.GlobularSet.cutoffFace_high line 20
  4. theorem OAI.Grothendieck.GlobularSet.coord_face line 27
  5. theorem OAI.Grothendieck.GlobularSet.cutoffLow_face line 36
  6. theorem OAI.Grothendieck.GlobularSet.cutoff_seam_face line 43
  7. theorem OAI.Grothendieck.GlobularSet.cutoff_high_face line 51
  8. theorem OAI.Grothendieck.GlobularSet.cutoffLow_parallel line 58
  9. theorem OAI.Grothendieck.GlobularSet.cutoff_boundary_seam_bijective line 76
  10. theorem OAI.Grothendieck.GlobularSet.cutoff_boundary_bijective line 117
  11. theorem OAI.Grothendieck.GlobularSet.faceMap_parallel line 151
  12. def OAI.Grothendieck.GlobularSet.cutoffUnitCell line 162
  13. theorem OAI.Grothendieck.GlobularSet.cutoffUnitCell_low line 169
  14. theorem OAI.Grothendieck.GlobularSet.cutoffUnitCell_high line 176
  15. theorem OAI.Grothendieck.GlobularSet.cutoffUnitCell_face line 183
  16. def OAI.Grothendieck.GlobularSet.cutoffUnit line 213
  17. theorem OAI.Grothendieck.GlobularSet.cutoffUnit_bijective line 218
  18. theorem OAI.Grothendieck.GlobularSet.Hom.evalFace_app line 227
  19. def OAI.Grothendieck.GlobularSet.Hom.presheafMap line 244
  20. def OAI.Grothendieck.GlobularPresheaf.tupleCellEquiv line 252
  21. def OAI.Grothendieck.GlobularPresheaf.tuplesMap line 283
  22. theorem OAI.Grothendieck.GlobularPresheaf.tupleCellEquiv_map line 288
  23. theorem OAI.Grothendieck.GlobularPresheaf.tupleCellEquiv_face line 293
  24. def OAI.Grothendieck.GlobularPresheaf.tupleUnderlyingMap line 310
  25. theorem OAI.Grothendieck.GlobularPresheaf.tuplesMap_bijective_globe line 316