OAI/Geometry/Borsuk/TenLabels/Labels.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BorsukNine.FiniteObstruction.Labels line 8
2. abbrev OAI.BorsukNine.FiniteObstruction.Family line 9
3. structure OAI.BorsukNine.FiniteObstruction.TenSystem line 13
4. lemma OAI.BorsukNine.FiniteObstruction.filter_card_eq_two_three_pos line 26
5. lemma OAI.BorsukNine.FiniteObstruction.filter_card_eq_two_three_neg line 40
6. lemma OAI.BorsukNine.FiniteObstruction.three_pos line 54
7. lemma OAI.BorsukNine.FiniteObstruction.three_neg line 64
8. lemma OAI.BorsukNine.FiniteObstruction.tetra_extension line 71
9. lemma OAI.BorsukNine.FiniteObstruction.map_compl line 83
10. lemma OAI.BorsukNine.FiniteObstruction.map_symm_map line 88
11. lemma OAI.BorsukNine.FiniteObstruction.symm_map_map line 93
12. lemma OAI.BorsukNine.FiniteObstruction.TenSystem.relabel line 98