OAI/Geometry/Cannon/PlaneTopology/Lift.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonWinding.lift line 18
  2. lemma OAI.CannonWinding.lift_exp line 21
  3. def OAI.CannonWinding.turn line 24
  4. lemma OAI.CannonWinding.turn_eq_of_lift line 26
  5. lemma OAI.CannonWinding.turn_const line 37
  6. lemma OAI.CannonWinding.turn_homotopy line 41
  7. lemma OAI.CannonWinding.turn_integer line 58
  8. lemma OAI.CannonWinding.turn_standard_loop line 63
  9. def OAI.CannonWinding.direction line 73
  10. lemma OAI.CannonWinding.direction_coe line 83
  11. lemma OAI.CannonWinding.direction_congr line 86
  12. def OAI.CannonWinding.winding line 91
  13. lemma OAI.CannonWinding.winding_homotopy line 94
  14. lemma OAI.CannonWinding.winding_moving_point line 106
  15. lemma OAI.CannonWinding.winding_const line 116
  16. lemma OAI.CannonWinding.winding_eq_of_homotopy line 129
  17. theorem OAI.CannonWinding.winding_locally_constant line 137
  18. lemma OAI.CannonWinding.winding_convex_zero line 156
  19. def OAI.CannonWinding.roundLoop line 174
  20. lemma OAI.CannonWinding.roundLoop_closed line 177
  21. lemma OAI.CannonWinding.roundLoop_dist line 180
  22. lemma OAI.CannonWinding.center_not_roundLoop line 184
  23. lemma OAI.CannonWinding.winding_roundLoop_center line 190
  24. lemma OAI.CannonWinding.winding_roundLoop_inside line 203
  25. lemma OAI.CannonWinding.winding_stable_near line 228
  26. def OAI.CannonWinding.index line 253
  27. lemma OAI.CannonWinding.index_eq line 257
  28. lemma OAI.CannonWinding.index_eventually_eq line 260
  29. lemma OAI.CannonWinding.index_zero_outside_closedBall line 275
  30. lemma OAI.CannonWinding.index_near_roundLoop line 284
  31. def OAI.CannonWinding.chartIndex line 303
  32. lemma OAI.CannonWinding.chartIndex_apply line 308
  33. lemma OAI.CannonWinding.chartIndex_zero_off_disk line 313
  34. lemma OAI.CannonWinding.chartIndex_eventually_eq line 327
  35. theorem OAI.CannonWinding.chartIndex_eq_on_preconnected line 350
  36. theorem OAI.CannonWinding.near_roundLoop_separates line 363
  37. lemma OAI.CannonWinding.chart_loop_neighborhood line 387
  38. def OAI.CannonWinding.complexPlane line 411
  39. lemma OAI.CannonWinding.small_complex_chart line 416
  40. theorem OAI.CannonWinding.uniform_robust_separating_loops line 442
  41. theorem OAI.CannonWinding.loop_approximation_separates line 504