OAI/Combinatorics/KMedian/Expanders/WalkSegments.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.PortGraph.Walk.segment line 16
  2. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.segment_vertex line 21
  3. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.segment_port line 23
  4. def OAI.MetricKMedian.PCP.PortGraph.Walk.catVertex line 26
  5. def OAI.MetricKMedian.PCP.PortGraph.Walk.catPort line 29
  6. def OAI.MetricKMedian.PCP.PortGraph.Walk.concat line 33
  7. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.concat_start line 56
  8. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.concat_end line 59
  9. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.segment_concat_left line 66
  10. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.segment_concat_right line 74
  11. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.concat_segments line 89
  12. def OAI.MetricKMedian.PCP.PortGraph.Walk.splitEquiv line 103