OAI/Geometry/SingularHomology/SimplexSubdivisionMesh.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.SimplexSubdivision.faceCenter line 13
2. lemma OAI.Problem340.SimplexSubdivision.faceCenter_eq line 16
3. lemma OAI.Problem340.SimplexSubdivision.card_smul_faceCenter line 20
4. lemma OAI.Problem340.SimplexSubdivision.sum_sub_faceCenter line 25
5. lemma OAI.Problem340.SimplexSubdivision.faceCenter_mem_convexHull line 30
6. lemma OAI.Problem340.SimplexSubdivision.dist_faceCenter_le line 37
7. lemma OAI.Problem340.SimplexSubdivision.card_smul_faceCenter_sub line 44
8. lemma OAI.Problem340.SimplexSubdivision.dist_faceCenter_nested_le line 57
9. lemma OAI.Problem340.SimplexSubdivision.dist_faceCenter_nested_le_mesh line 89
10. lemma OAI.Problem340.SimplexSubdivision.diam_faceCenter_chain_le line 105
11. lemma OAI.Problem340.SimplexSubdivision.dist_faceCenter_of_mem_convexHull_le_mesh line 125
12. lemma OAI.Problem340.SimplexSubdivision.diam_convexHull_insert_faceCenter_le_mesh line 140