OAI/Analysis/SegmentLenses/TreeGeometry.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Ancestry, segment splitting, and opposite crossings

  1. class OAI.SegmentLenses.TreeOrder line 20
  2. class OAI.SegmentLenses.IntervalSegments line 24
  3. instance OAI.SegmentLenses.infiniteOrder line 27
  4. instance OAI.SegmentLenses.infiniteTreeOrder line 34
  5. instance OAI.SegmentLenses.infiniteIntervalSegments line 37
  6. instance OAI.SegmentLenses.infiniteLocallyFinite line 40
  7. instance OAI.SegmentLenses.forestOrder line 46
  8. instance OAI.SegmentLenses.forestTreeOrder line 53
  9. instance OAI.SegmentLenses.forestIntervalSegments line 60
  10. instance OAI.SegmentLenses.forestLocallyFinite line 63
  11. theorem OAI.SegmentLenses.interval_isSegment line 81
  12. theorem OAI.SegmentLenses.halfOpen_isSegment line 90
  13. theorem OAI.SegmentLenses.split_interval line 121
  14. theorem OAI.SegmentLenses.split_disjoint line 139
  15. theorem OAI.SegmentLenses.head_zero_above line 149
  16. theorem OAI.SegmentLenses.segment_sum_eq_head line 163
  17. theorem OAI.SegmentLenses.split_suffix_sum line 177
  18. theorem OAI.SegmentLenses.opposite_split_gain line 186
  19. theorem OAI.SegmentLenses.selected_split_budget line 205
  20. theorem OAI.SegmentLenses.matched_opposite_crossing line 276
  21. def OAI.SegmentLenses.Gate line 328
  22. theorem OAI.SegmentLenses.gates_incomparable line 331
  23. theorem OAI.SegmentLenses.gate_unique_in_interval line 340
  24. def OAI.SegmentLenses.SegmentFamily.presentation line 350
  25. def OAI.SegmentLenses.SegmentFamily.first line 358
  26. def OAI.SegmentLenses.SegmentFamily.last line 360
  27. theorem OAI.SegmentLenses.SegmentFamily.first_le_last line 362
  28. theorem OAI.SegmentLenses.SegmentFamily.repr line 368
  29. theorem OAI.SegmentLenses.SegmentFamily.repr_disjoint line 374
  30. def OAI.SegmentLenses.SegmentFamily.boundary line 383
  31. theorem OAI.SegmentLenses.SegmentFamily.boundary_of_mem line 386
  32. theorem OAI.SegmentLenses.SegmentFamily.boundary_nonzero line 404
  33. theorem OAI.SegmentLenses.SegmentFamily.gate_unique line 418
  34. theorem OAI.SegmentLenses.opposite_crossing line 428