OAI/Geometry/SingularHomology/SubdivisionSubtypeMesh.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem340.SingularSubdivision.mapVertices_eq_mapDomain line 12
2. lemma OAI.Problem340.SingularSubdivision.mem_support_mapVertices_iff_of_injective line 18
3. lemma OAI.Problem340.SingularSubdivision.coe_simplexCenters line 27
4. lemma OAI.Problem340.SingularSubdivision.coe_subdivision line 37
5. lemma OAI.Problem340.SingularSubdivision.coe_subdivision_iterate line 43
6. theorem OAI.Problem340.SingularSubdivision.simplex_iterated_subdivision_support line 52
7. theorem OAI.Problem340.SingularSubdivision.simplex_subdivision_support_barycentricCell line 63