OAI/Geometry/Borsuk/Simplicial/Flip.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.flipAt line 10
2. lemma OAI.BorsukNine.SimplicialChains.flipAt_ne line 13
3. lemma OAI.BorsukNine.SimplicialChains.crossFacet_injective line 18
4. def OAI.BorsukNine.SimplicialChains.crossRidge line 26
5. lemma OAI.BorsukNine.SimplicialChains.crossRidge_card line 29
6. lemma OAI.BorsukNine.SimplicialChains.crossRidge_mem line 34
7. lemma OAI.BorsukNine.SimplicialChains.mem_crossRidge line 43
8. lemma OAI.BorsukNine.SimplicialChains.crossRidge_subset_iff line 54
9. lemma OAI.BorsukNine.SimplicialChains.crossRidge_parents line 66
10. lemma OAI.BorsukNine.SimplicialChains.boundary_ridge_coefficient line 87
11. lemma OAI.BorsukNine.SimplicialChains.cross_cycle_adjacent_coeff line 119