OAI/Geometry/Borsuk/Support/ChamberPath.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.chamberPath line 11
2. lemma OAI.BorsukNine.signChamber_smul line 14
3. lemma OAI.BorsukNine.chamber_interpolation_mem line 20
4. lemma OAI.BorsukNine.chamber_interpolation_ne_zero line 25
5. lemma OAI.BorsukNine.chamberPath_norm line 32
6. lemma OAI.BorsukNine.chamberPath_mem line 38
7. lemma OAI.BorsukNine.chamberPath_zero line 44
8. lemma OAI.BorsukNine.chamberPath_one line 47
9. lemma OAI.BorsukNine.chamber_add_ne_zero line 50
10. lemma OAI.BorsukNine.chamberPath_continuousOn line 60