OAI/GroupTheory/SimpleAmenable/Simplicial/NestedPosReindex.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RestrictedNerve.inclusion_η line 18
  2. lemma OAI.RestrictedNerve.inclusion_μ line 20
  3. lemma OAI.RestrictedNerve.widePosReindex_η line 22
  4. lemma OAI.RestrictedNerve.widePosReindex_μ line 24
  5. lemma OAI.RestrictedNerve.posReindex_η line 26
  6. lemma OAI.RestrictedNerve.posReindex_μ line 28
  7. lemma OAI.RestrictedNerve.eqToHom_pos_app line 30
  8. def OAI.RestrictedNerve.nestedPosReindex line 34
  9. lemma OAI.RestrictedNerve.nestedPosReindex_property line 70
  10. lemma OAI.RestrictedNerve.nestedPosReindex_inclusion_obj line 74
  11. lemma OAI.RestrictedNerve.nestedPosReindex_inclusion line 89
  12. lemma OAI.RestrictedNerve.transpose_η_app line 103
  13. lemma OAI.RestrictedNerve.transpose_obj line 110
  14. lemma OAI.RestrictedNerve.transpose_map line 112
  15. lemma OAI.RestrictedNerve.diagramReindex_η line 114
  16. lemma OAI.RestrictedNerve.diagramReindex_μ line 116
  17. abbrev OAI.RestrictedNerve.innerReindexLeft line 118
  18. abbrev OAI.RestrictedNerve.innerReindexRight line 122
  19. lemma OAI.RestrictedNerve.doubleTranspose_innerReindex_vertex line 128
  20. lemma OAI.RestrictedNerve.nested_comp_app line 152
  21. lemma OAI.RestrictedNerve.nested_eqToHom_app line 157
  22. lemma OAI.RestrictedNerve.twiceTransposed_comp_app line 165
  23. lemma OAI.RestrictedNerve.twiceTransposed_eqToHom_app line 172
  24. lemma OAI.RestrictedNerve.doubleTranspose_innerReindex_obj line 181
  25. lemma OAI.RestrictedNerve.twiceTransposed_transport_ext line 194
  26. lemma OAI.RestrictedNerve.doubleTranspose_innerReindex_eq line 212
  27. lemma OAI.RestrictedNerve.doubleTranspose_innerReindex line 222
  28. lemma OAI.IntervalBar.Diagram.map_ε line 243
  29. lemma OAI.IntervalBar.Diagram.map_μ line 245
  30. lemma OAI.IntervalBar.Diagram.reindex_ε line 247
  31. lemma OAI.IntervalBar.Diagram.reindex_μ line 249
  32. instance OAI.IntervalBar.Diagram.reindex_map_monoidal line 251
  33. lemma OAI.IntervalBar.Diagram.map_reindex_map line 271