OAI/Geometry/Borsuk/Projectors/RaySet.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.raySet line 11
2. lemma OAI.BorsukNine.raySet_isClosed line 13
3. lemma OAI.BorsukNine.mem_raySet_iff line 15
4. def OAI.BorsukNine.matrixRayFibre line 36
5. lemma OAI.BorsukNine.matrixRayFibre_closed line 39
6. lemma OAI.BorsukNine.Admissible.facet_support line 45
7. lemma OAI.BorsukNine.matrixRayFibre_representative line 55
8. lemma OAI.BorsukNine.Admissible.matrixRayFibre_subset_patch line 60