OAI/GroupTheory/SimpleAmenable/Simplicial/MonoidNerveCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MonoidNerveCoordinates.Simplex line 10
2. def OAI.MonoidNerveCoordinates.labels line 11
3. def OAI.MonoidNerveCoordinates.ofLabels line 12
4. lemma OAI.MonoidNerveCoordinates.eqToHom_val line 14
5. lemma OAI.MonoidNerveCoordinates.labels_ofLabels line 15
6. lemma OAI.MonoidNerveCoordinates.ofLabels_labels line 18
7. def OAI.MonoidNerveCoordinates.equiv line 24
8. lemma OAI.MonoidNerveCoordinates.labels_zero_face line 29
9. lemma OAI.MonoidNerveCoordinates.map_congr line 31
10. lemma OAI.MonoidNerveCoordinates.labels_last_face line 36