OAI/Geometry/Borsuk/MatrixGeometry/FibreContinuity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.Admissible.negativeCoordinates_continuousOn line 15
2. lemma OAI.BorsukNine.centeredFibre_continuousOn line 23
3. lemma OAI.BorsukNine.fibreTransport_continuousOn_comp line 28
4. lemma OAI.BorsukNine.chamberPath_matrix_continuousOn line 38
5. lemma OAI.BorsukNine.transportedFibre_continuousOn line 50
6. lemma OAI.BorsukNine.Admissible.fibreHomotopy_continuousOn line 62