OAI/Geometry/Borsuk/Simplicial/CrossChainDimensionBound.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.SimplicialChains.cross_chain_dimension_bound line 8
2. def OAI.BorsukNine.SimplicialChains.barycenter line 45
3. lemma OAI.BorsukNine.SimplicialChains.barycenter_eq_centerMass line 47
4. lemma OAI.BorsukNine.SimplicialChains.barycenter_mem_convex line 51
5. lemma OAI.BorsukNine.SimplicialChains.barycenter_norm_le line 59
6. lemma OAI.BorsukNine.SimplicialChains.barycenter_inner line 65
7. def OAI.BorsukNine.SimplicialChains.hemisphereComplex line 71
8. lemma OAI.BorsukNine.SimplicialChains.hemisphere_vertex_nonzero line 79
9. lemma OAI.BorsukNine.SimplicialChains.hemisphere_barycenter line 86
10. lemma OAI.BorsukNine.SimplicialChains.barycenter_sub_eq line 93
11. lemma OAI.BorsukNine.SimplicialChains.barycenter_dist_vertex line 99
12. lemma OAI.BorsukNine.SimplicialChains.barycenter_dist_carrier line 124
13. lemma OAI.BorsukNine.SimplicialChains.barycenter_mesh_factor line 132