OAI/Geometry/Borsuk/Simplicial/LinearMapSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.SimplicialChains.linearMap_eq_of_support line 11
2. lemma OAI.BorsukNine.SimplicialChains.mapChains_boundary_simplex_of_image line 20
3. lemma OAI.BorsukNine.SimplicialChains.mapChains_boundary_of_support line 40
4. lemma OAI.BorsukNine.SimplicialChains.mapChains_augmentation_simplex_of_image line 50
5. lemma OAI.BorsukNine.SimplicialChains.mapChains_augmentation_of_support line 64
6. lemma OAI.BorsukNine.SimplicialChains.mapChains_degree_all line 73
7. lemma OAI.BorsukNine.SimplicialChains.mapChains_equivariant line 84
8. lemma OAI.BorsukNine.SimplicialChains.mapChains_norm line 110