OAI/Geometry/Cannon/PlaneTopology/Reverse.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CannonEmbeddedArc.Arc.reverse line 52
2. lemma OAI.CannonEmbeddedArc.Arc.reverse_apply line 55
3. lemma OAI.CannonEmbeddedArc.Arc.reverse_zero line 56
4. lemma OAI.CannonEmbeddedArc.Arc.reverse_one line 57
5. lemma OAI.CannonEmbeddedArc.Arc.reverse_range line 58
6. lemma OAI.CannonEmbeddedArc.Arc.local_arc_flat line 61
7. lemma OAI.CannonEmbeddedArc.Arc.pair_start_local_arc line 74
8. lemma OAI.CannonEmbeddedArc.Arc.pair_start_flat line 150
9. theorem OAI.CannonEmbeddedArc.Arc.pair_flat_at_left line 160
10. theorem OAI.CannonEmbeddedArc.Arc.pair_incident_labels line 187
11. theorem OAI.CannonEmbeddedArc.Arc.pair_labels_surjective line 231
12. lemma OAI.CannonEmbeddedArc.Arc.centered_chord_endpoints line 258
13. lemma OAI.CannonEmbeddedArc.Arc.centered_chord_ball line 272
14. theorem OAI.CannonEmbeddedArc.Arc.pair_isolated_chord line 297
15. lemma OAI.CannonWinding.turn_path_trans line 396
16. lemma OAI.CannonWinding.winding_path_trans line 417
17. lemma OAI.CannonWinding.winding_path_homotopy line 441
18. def OAI.CannonWinding.blendPaths line 449
19. def OAI.CannonWinding.upperSemi line 464
20. def OAI.CannonWinding.lowerSemi line 470
21. lemma OAI.CannonWinding.upperSemi_norm line 479
22. lemma OAI.CannonWinding.lowerSemi_norm line 480
23. lemma OAI.CannonWinding.upperSemi_im line 481
24. lemma OAI.CannonWinding.lowerSemi_im line 486
25. lemma OAI.CannonWinding.winding_upperSemi line 493
26. lemma OAI.CannonWinding.winding_lowerSemi line 513
27. lemma OAI.CannonWinding.path_outside_avoids line 538
28. lemma OAI.CannonWinding.winding_outside_move line 543
29. lemma OAI.CannonWinding.segment_diameter_im line 559
30. theorem OAI.CannonWinding.winding_chord_replace line 562
31. theorem OAI.CannonWinding.chord_winding_jump line 610
32. lemma OAI.CannonWinding.winding_on_component line 634
33. theorem OAI.CannonWinding.chord_separates line 650