OAI/Geometry/Borsuk/Simplicial/F2.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BorsukNine.SimplicialChains.F₂ line 9
2. abbrev OAI.BorsukNine.SimplicialChains.Chain line 10
3. def OAI.BorsukNine.SimplicialChains.simplex line 12
4. lemma OAI.BorsukNine.SimplicialChains.simplex_of_mem line 17
5. lemma OAI.BorsukNine.SimplicialChains.simplex_empty line 21
6. def OAI.BorsukNine.SimplicialChains.boundary line 25
7. lemma OAI.BorsukNine.SimplicialChains.boundary_simplex line 29
8. lemma OAI.BorsukNine.SimplicialChains.boundary_simplex_subset line 34
9. lemma OAI.BorsukNine.SimplicialChains.chain_add_self line 43
10. lemma OAI.BorsukNine.SimplicialChains.double_erase_sum line 47
11. lemma OAI.BorsukNine.SimplicialChains.boundary_twice_simplex line 76
12. lemma OAI.BorsukNine.SimplicialChains.boundary_sq line 86
13. def OAI.BorsukNine.SimplicialChains.augmentation line 95
14. lemma OAI.BorsukNine.SimplicialChains.augmentation_simplex line 99
15. lemma OAI.BorsukNine.SimplicialChains.augmentation_simplex_subset line 104
16. lemma OAI.BorsukNine.SimplicialChains.augmentation_boundary_simplex line 111
17. lemma OAI.BorsukNine.SimplicialChains.augmentation_boundary line 125