OAI/Combinatorics/KMedian/Expanders/GraphExtend.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedian.PCP.extend_involutive line 12
  2. def OAI.MetricKMedian.PCP.PortGraph.portEmbed line 27
  3. def OAI.MetricKMedian.PCP.PortGraph.extend line 29
  4. lemma OAI.MetricKMedian.PCP.PortGraph.extend_rotate_image line 33
  5. lemma OAI.MetricKMedian.PCP.PortGraph.extend_step_image line 37
  6. lemma OAI.MetricKMedian.PCP.PortGraph.portEmbed_range line 42
  7. lemma OAI.MetricKMedian.PCP.PortGraph.extend_rotate_outside line 49
  8. def OAI.MetricKMedian.PCP.PortCSP.extendedAllowed line 59
  9. lemma OAI.MetricKMedian.PCP.PortCSP.extendedAllowed_image line 64
  10. lemma OAI.MetricKMedian.PCP.PortCSP.extendedAllowed_outside line 71
  11. def OAI.MetricKMedian.PCP.PortCSP.extend line 75
  12. lemma OAI.MetricKMedian.PCP.PortCSP.extend_bad_image line 89
  13. lemma OAI.MetricKMedian.PCP.PortCSP.extend_complete line 98