OAI/Analysis/PlanarPacking/BarrierEndpoints.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpPlanar.P_period line 8
2. lemma OAI.SharpPlanar.P_reflect line 11
3. lemma OAI.SharpPlanar.P_half line 14
4. lemma OAI.SharpPlanar.P_two line 21
5. lemma OAI.SharpPlanar.P_eight line 22
6. lemma OAI.SharpPlanar.P_short_lower line 25
7. lemma OAI.SharpPlanar.P_long_lower line 31
8. lemma OAI.SharpPlanar.P_other_midpoints line 51
9. lemma OAI.SharpPlanar.barrier_endpoints line 61