OAI/GroupTheory/SimpleAmenable/Simplicial/StringEvaluation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RestrictedNerve.stringEvaluation line 16
  2. lemma OAI.RestrictedNerve.stringEvaluation_obj line 21
  3. lemma OAI.RestrictedNerve.stringEvaluation_map line 23
  4. instance OAI.RestrictedNerve.stringEvaluationMonoidal line 30
  5. instance OAI.RestrictedNerve.stringEvaluationBraided line 39
  6. lemma OAI.RestrictedNerve.stringEvaluation_η line 45
  7. lemma OAI.RestrictedNerve.stringEvaluation_ε line 48
  8. lemma OAI.RestrictedNerve.stringEvaluation_μ line 51
  9. lemma OAI.RestrictedNerve.transpose_evaluation line 54
  10. lemma OAI.RestrictedNerve.restrictionInclusion_ε line 80
  11. instance OAI.RestrictedNerve.transpose_evaluation_monoidal line 82
  12. lemma OAI.RestrictedNerve.tripleTranspose_evaluation line 108
  13. def OAI.RestrictedNerve.tripleInnerReindex line 145
  14. lemma OAI.RestrictedNerve.tripleResolutionAugmentation_inner_natural line 156