OAI/Geometry/TranslativeCovering/ProjectiveCaps.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProjectiveCaps.angle line 26
2. lemma OAI.ProjectiveCaps.angle_nonneg line 29
3. lemma OAI.ProjectiveCaps.angle_self line 32
4. lemma OAI.ProjectiveCaps.angle_comm line 36
5. lemma OAI.ProjectiveCaps.angle_triangle line 40
6. def OAI.ProjectiveCaps.costDist line 62
7. lemma OAI.ProjectiveCaps.costDist_nonneg line 65
8. lemma OAI.ProjectiveCaps.costDist_self line 69
9. lemma OAI.ProjectiveCaps.costDist_comm line 73
10. lemma OAI.ProjectiveCaps.costDist_triangle line 77