OAI/GroupTheory/SimpleAmenable/Simplicial/IntervalEdge.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IntervalBar.Diagram.interval line 11
  2. def OAI.IntervalBar.Diagram.pairAt line 14
  3. lemma OAI.IntervalBar.Diagram.interval_congr line 19
  4. def OAI.IntervalBar.Diagram.faceEdge line 21
  5. lemma OAI.IntervalBar.Diagram.faceEdge_left line 24
  6. lemma OAI.IntervalBar.Diagram.faceEdge_right line 30
  7. def OAI.IntervalBar.Diagram.faceEdge_middle line 36
  8. def OAI.IntervalBar.Diagram.faceEdgeIso line 50
  9. abbrev OAI.NerveHomology.map line 67
  10. lemma OAI.NerveHomology.comp line 68
  11. lemma OAI.NerveHomology.iso line 71
  12. lemma OAI.NerveHomology.const line 73
  13. lemma OAI.MarkedH1.primitive_eval line 83
  14. lemma OAI.MarkedH1.recognition line 88
  15. lemma OAI.MarkedH1.recognition_const line 97
  16. def OAI.MarkedH1.wordDiagram_eval line 103
  17. def OAI.MarkedH1.primitiveFace_eval line 106
  18. def OAI.MarkedH1.includeProjIso line 112
  19. def OAI.MarkedH1.wordPair_left line 116
  20. def OAI.MarkedH1.wordPair_right line 122
  21. def OAI.MarkedH1.wordPair_other line 128
  22. lemma OAI.MarkedH1.face_recognition line 135
  23. lemma OAI.MarkedH1.face_recognition_const line 144