OAI/Computability/MinUncut/Graphs/GraphOutput.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.PathRealization.output line 13
  2. def OAI.MinUncut.PathRealization.edgePair line 21
  3. lemma OAI.MinUncut.PathRealization.edgePair_sym line 25
  4. lemma OAI.MinUncut.PathRealization.edgePair_injective line 30
  5. lemma OAI.MinUncut.PathRealization.edgePair_lt line 38
  6. lemma OAI.MinUncut.PathRealization.output_adjacent_iff line 49
  7. lemma OAI.MinUncut.PathRealization.output_forward_edge_iff line 63
  8. lemma OAI.MinUncut.PathRealization.edgePair_mono line 79
  9. lemma OAI.MinUncut.PathRealization.output_uncut line 90
  10. lemma OAI.MinUncut.PathRealization.output_opt_le line 111
  11. lemma OAI.MinUncut.PathRealization.le_output_opt line 114
  12. lemma OAI.MinUncut.PathRealization.output_yes line 121
  13. lemma OAI.MinUncut.PathRealization.output_no line 130
  14. def OAI.MinUncut.FiniteProof.multiplicity line 144
  15. lemma OAI.MinUncut.FiniteProof.multiplicity_cast line 146
  16. abbrev OAI.MinUncut.FiniteProof.UnitDemand line 157
  17. def OAI.MinUncut.FiniteProof.expanded line 159
  18. lemma OAI.MinUncut.FiniteProof.expanded_failure line 162
  19. lemma OAI.MinUncut.FiniteProof.expanded_weight line 166
  20. lemma OAI.MinUncut.FiniteProof.expanded_card line 178
  21. lemma OAI.MinUncut.FiniteProof.expanded_card_cast line 182
  22. lemma OAI.MinUncut.FiniteProof.threshold_positive line 193
  23. def OAI.MinUncut.FiniteProof.rationalGraph line 195
  24. lemma OAI.MinUncut.FiniteProof.rationalGraph_threshold line 198
  25. lemma OAI.MinUncut.FiniteProof.rationalGraph_vertices line 201
  26. lemma OAI.MinUncut.FiniteProof.rationalGraph_yes line 205
  27. lemma OAI.MinUncut.FiniteProof.rationalGraph_no line 216