OAI/Geometry/Borsuk/Simplicial/LabelRegion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.labelRegion line 9
2. lemma OAI.BorsukNine.SimplicialChains.labelRegion_closed line 13
3. lemma OAI.BorsukNine.SimplicialChains.sphereLabel_mem_region line 24
4. lemma OAI.BorsukNine.SimplicialChains.compact_label_locality line 39
5. lemma OAI.BorsukNine.SimplicialChains.mapSimplex_coeff_zero_of_ne line 83
6. lemma OAI.BorsukNine.SimplicialChains.image_ne_crossFacet_of_missing line 90
7. lemma OAI.BorsukNine.SimplicialChains.localized_approximation_coeff line 100