OAI/GroupTheory/SimpleAmenable/Simplicial/Supplemental.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RestrictedNerve.tripleInnerReindex_id line 17
  2. lemma OAI.RestrictedNerve.tripleInnerReindex_comp line 21
  3. def OAI.RestrictedNerve.innerResolutionRows line 28
  4. def OAI.RestrictedNerve.innerNerveRows line 37
  5. def OAI.RestrictedNerve.innerResolutionAugmentation line 51
  6. instance OAI.RestrictedNerve.innerResolutionTotal_isIso line 55
  7. lemma OAI.RestrictedNerve.tripleInnerMiddle_commute line 63
  8. def OAI.RestrictedNerve.innerRowsMiddle line 69
  9. def OAI.RestrictedNerve.innerNerveRowsMiddle line 77
  10. lemma OAI.RestrictedNerve.innerResolutionAugmentation_middle_natural line 85
  11. lemma OAI.RestrictedNerve.innerRowsMiddle_id line 91
  12. lemma OAI.RestrictedNerve.innerRowsMiddle_comp line 99
  13. def OAI.RestrictedNerve.middleResolutionRows line 110
  14. lemma OAI.RestrictedNerve.innerNerveRowsMiddle_id line 120
  15. lemma OAI.RestrictedNerve.innerNerveRowsMiddle_comp line 127
  16. def OAI.RestrictedNerve.middleNerveRows line 136
  17. def OAI.RestrictedNerve.middleResolutionAugmentation line 145
  18. instance OAI.RestrictedNerve.middleResolutionTotal_isIso line 153
  19. lemma OAI.RestrictedNerve.tripleInnerOuter_commute line 161
  20. lemma OAI.RestrictedNerve.tripleMiddleOuter_commute line 167
  21. def OAI.RestrictedNerve.innerRowsOuter line 173
  22. def OAI.RestrictedNerve.innerNerveRowsOuter line 181
  23. lemma OAI.RestrictedNerve.innerResolutionAugmentation_outer_natural line 189
  24. lemma OAI.RestrictedNerve.innerRowsMiddleOuter_commute line 195
  25. lemma OAI.RestrictedNerve.innerNerveRowsMiddleOuter_commute line 204
  26. def OAI.RestrictedNerve.middleRowsOuter line 212
  27. def OAI.RestrictedNerve.middleNerveRowsOuter line 220
  28. lemma OAI.RestrictedNerve.middleResolutionAugmentation_outer_natural line 228
  29. lemma OAI.RestrictedNerve.innerRowsOuter_id line 238
  30. lemma OAI.RestrictedNerve.innerRowsOuter_comp line 246
  31. lemma OAI.RestrictedNerve.middleRowsOuter_id line 257
  32. lemma OAI.RestrictedNerve.middleRowsOuter_comp line 262
  33. lemma OAI.RestrictedNerve.innerNerveRowsOuter_id line 269
  34. lemma OAI.RestrictedNerve.innerNerveRowsOuter_comp line 276
  35. lemma OAI.RestrictedNerve.middleNerveRowsOuter_id line 285
  36. lemma OAI.RestrictedNerve.middleNerveRowsOuter_comp line 291
  37. def OAI.RestrictedNerve.outerResolutionRows line 299
  38. def OAI.RestrictedNerve.outerNerveRows line 308
  39. def OAI.RestrictedNerve.outerResolutionAugmentation line 317
  40. instance OAI.RestrictedNerve.tripleResolutionTotal_isIso line 326
  41. lemma OAI.RestrictedNerve.reverseDiagonalReindex line 338
  42. def OAI.RestrictedNerve.totalNerveBarIso line 347
  43. def OAI.RestrictedNerve.totalStringToBar line 356
  44. instance OAI.RestrictedNerve.totalStringToBar_isIso line 359
  45. instance OAI.SimpleAmenable.PolygonObject.positionalPropertyInverse line 372
  46. def OAI.SimpleAmenable.PolygonObject.tripleStringToBar line 380
  47. instance OAI.SimpleAmenable.PolygonObject.tripleStringToBar_isIso line 384
  48. def OAI.RestrictedNerve.stringBarRows line 396
  49. def OAI.RestrictedNerve.stringBarTotalComponent line 409