OAI/Geometry/Cannon/PlaneTopology/Consecutive.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonEmbeddedArc.Arc.interval_of_ordConnected line 18
  2. lemma OAI.CannonEmbeddedArc.Arc.intersection_ordConnected_symm line 26
  3. theorem OAI.CannonEmbeddedArc.Arc.finite_breakpoints line 33
  4. def OAI.CannonEmbeddedArc.Arc.Consecutive line 69
  5. lemma OAI.CannonEmbeddedArc.Arc.consecutive_cover line 72
  6. lemma OAI.CannonEmbeddedArc.Arc.convexComb_sliceParam line 99
  7. lemma OAI.CannonEmbeddedArc.Arc.subarc_range_eq line 103
  8. lemma OAI.CannonEmbeddedArc.Arc.Consecutive.ordered line 113
  9. lemma OAI.CannonEmbeddedArc.Arc.ordered_subarcs_meeting line 125
  10. lemma OAI.CannonEmbeddedArc.Arc.ordered_subarcs_compatible line 141
  11. def OAI.CannonEmbeddedArc.Arc.segments line 157
  12. lemma OAI.CannonEmbeddedArc.Arc.mem_segments line 161
  13. lemma OAI.CannonEmbeddedArc.Arc.segments_card line 168
  14. lemma OAI.CannonEmbeddedArc.Arc.segment_consecutive line 172
  15. def OAI.CannonEmbeddedArc.Arc.subdivArc line 175
  16. lemma OAI.CannonEmbeddedArc.Arc.subdivArc_zero line 178
  17. lemma OAI.CannonEmbeddedArc.Arc.subdivArc_one line 180
  18. lemma OAI.CannonEmbeddedArc.Arc.subdivArc_range_eq line 183
  19. lemma OAI.CannonEmbeddedArc.Arc.subdivision_cover line 187
  20. lemma OAI.CannonEmbeddedArc.Arc.subdivision_compatible line 201
  21. lemma OAI.CannonEmbeddedArc.Arc.convexComb_injective line 211
  22. lemma OAI.CannonEmbeddedArc.Arc.Consecutive.marked_parameter line 219
  23. lemma OAI.CannonEmbeddedArc.Arc.subarc_parameter_endpoint line 230
  24. lemma OAI.CannonEmbeddedArc.Arc.Compatible.subarcs line 240
  25. lemma OAI.CannonEmbeddedArc.Arc.Consecutive.interval_dichotomy line 250
  26. lemma OAI.CannonEmbeddedArc.Arc.free_segment_intersection line 266
  27. theorem OAI.CannonEmbeddedArc.Arc.old_breakpoints line 306
  28. lemma OAI.CannonEmbeddedArc.Arc.free_segment_compatible_old_subdivision line 327
  29. lemma OAI.CannonEmbeddedArc.Arc.subdivArc_range_subset line 353
  30. lemma OAI.CannonEmbeddedArc.Arc.Compatible.of_disjoint line 357
  31. def OAI.CannonEmbeddedArc.Arc.Vertex line 365
  32. lemma OAI.CannonEmbeddedArc.Arc.subdivision_mark_vertex line 368
  33. def OAI.CannonEmbeddedArc.Arc.FreeSegment line 383
  34. def OAI.CannonEmbeddedArc.Arc.RefinementIndex line 386
  35. instance OAI.CannonEmbeddedArc.Arc.(instance at line 389) line 389
  36. def OAI.CannonEmbeddedArc.Arc.refinementArc line 394
  37. lemma OAI.CannonEmbeddedArc.Arc.refinement_compatible line 405
  38. lemma OAI.CannonEmbeddedArc.Arc.refinement_old_subset line 432
  39. lemma OAI.CannonEmbeddedArc.Arc.refinement_cover line 439
  40. lemma OAI.CannonEmbeddedArc.Arc.refinement_old_mark_vertex line 462
  41. lemma OAI.CannonEmbeddedArc.Arc.refinement_new_mark_vertex line 468
  42. lemma OAI.CannonEmbeddedArc.Arc.refinement_card line 486
  43. lemma OAI.CannonEmbeddedArc.Arc.range_subset_of_interior line 509
  44. lemma OAI.CannonEmbeddedArc.Arc.free_segment_original line 519
  45. def OAI.CannonEmbeddedArc.Arc.intersectionCount line 535
  46. lemma OAI.CannonEmbeddedArc.Arc.intersectionCount_eq_card line 539
  47. lemma OAI.CannonEmbeddedArc.Arc.sum_indicator_le_card line 545
  48. lemma OAI.CannonEmbeddedArc.Arc.refinement_local_count line 551