OAI/Geometry/SingularHomology/SimplexCoordinates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Problem340.RealSimplex.coordinatesFun line 19
2. def OAI.Problem340.RealSimplex.coordinates line 22
3. lemma OAI.Problem340.RealSimplex.single_apply line 25
4. lemma OAI.Problem340.RealSimplex.barycenter_apply line 30
5. lemma OAI.Problem340.RealSimplex.map_apply line 34
6. lemma OAI.Problem340.RealSimplex.coordinates_injective line 44
7. def OAI.Problem340.RealSimplex.coordinateSet line 47
8. lemma OAI.Problem340.RealSimplex.mem_coordinateSet line 50
9. lemma OAI.Problem340.RealSimplex.convex_coordinateSet line 54
10. def OAI.Problem340.RealSimplex.coordinateHomeomorph line 57
11. lemma OAI.Problem340.RealSimplex.coordinateHomeomorph_apply line 64
12. lemma OAI.Problem340.RealSimplex.coordinateHomeomorph_symm_apply line 67
13. instance OAI.Problem340.RealSimplex.metricSpace line 71
14. lemma OAI.Problem340.RealSimplex.coordinateHomeomorph_symm_apply_at line 74
15. lemma OAI.Problem340.RealSimplex.contractible line 78
16. lemma OAI.Problem340.RealSimplex.locallyPathConnected line 84