OAI/Geometry/Borsuk/Support/MixedHomotopy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.Admissible.cone_unit_positive line 19
2. lemma OAI.BorsukNine.Admissible.maximal_cone_zero line 26
3. lemma OAI.BorsukNine.traceSphere_weights line 40
4. def OAI.BorsukNine.mixedHomotopy line 44
5. lemma OAI.BorsukNine.Admissible.mixedHomotopy_zero line 49
6. lemma OAI.BorsukNine.Admissible.mixedHomotopy_nonzero line 84
7. lemma OAI.BorsukNine.Admissible.mixedHomotopy_continuousOn line 90