OAI/Combinatorics/MatchingCount/Graphs/Incident.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Enlargement.totalDeletionCharge_eq_blocks line 14
  2. theorem OAI.MatchingFPRAS.Enlargement.deletionConstant_eq_charge line 27
  3. theorem OAI.MatchingFPRAS.Enlargement.real_partition_charge_identity line 42
  4. abbrev OAI.MatchingFPRAS.Representation.Incident line 72
  5. def OAI.MatchingFPRAS.Representation.other line 74
  6. lemma OAI.MatchingFPRAS.Representation.other_source line 78
  7. lemma OAI.MatchingFPRAS.Representation.other_target line 79
  8. lemma OAI.MatchingFPRAS.Representation.other_incident line 82
  9. lemma OAI.MatchingFPRAS.Representation.other_ne line 86
  10. lemma OAI.MatchingFPRAS.Representation.other_other line 89
  11. lemma OAI.MatchingFPRAS.Representation.edge_eq_of_inc_other line 92
  12. lemma OAI.MatchingFPRAS.Representation.selected_not_hole line 110
  13. def OAI.MatchingFPRAS.Representation.chosen line 115
  14. lemma OAI.MatchingFPRAS.Representation.chosen_spec line 119
  15. lemma OAI.MatchingFPRAS.Representation.chosen_eq line 123
  16. def OAI.MatchingFPRAS.Representation.mateFun line 127
  17. lemma OAI.MatchingFPRAS.Representation.mateFun_hole line 131
  18. lemma OAI.MatchingFPRAS.Representation.mateFun_selected line 133
  19. lemma OAI.MatchingFPRAS.Representation.mateFun_involutive line 139
  20. def OAI.MatchingFPRAS.Representation.asMate line 148
  21. lemma OAI.MatchingFPRAS.Representation.asMate_holes line 150
  22. lemma OAI.MatchingFPRAS.Representation.asMate_selected line 160
  23. def OAI.MatchingFPRAS.Representation.select line 181
  24. lemma OAI.MatchingFPRAS.Representation.select_eq_true line 185
  25. lemma OAI.MatchingFPRAS.Representation.select_mate_other line 188
  26. lemma OAI.MatchingFPRAS.Representation.edge_eq_of_selected_inc line 196
  27. lemma OAI.MatchingFPRAS.Representation.select_holes line 211
  28. lemma OAI.MatchingFPRAS.Representation.select_asMate line 230
  29. lemma OAI.MatchingFPRAS.Representation.asMate_select line 235
  30. def OAI.MatchingFPRAS.Representation.matchingEquiv line 247
  31. lemma OAI.MatchingFPRAS.Representation.selection_weight line 255
  32. lemma OAI.MatchingFPRAS.Representation.asMate_weight line 278
  33. theorem OAI.MatchingFPRAS.Representation.logical_partition_eq line 282
  34. theorem OAI.MatchingFPRAS.Representation.logical_partition_forbidden_le line 293
  35. lemma OAI.MatchingFPRAS.Enlargement.pathConstant_pos line 333
  36. lemma OAI.MatchingFPRAS.Enlargement.intact_family line 337
  37. theorem OAI.MatchingFPRAS.Enlargement.intact_partition_identity line 351
  38. theorem OAI.MatchingFPRAS.Enlargement.lifted_hole_bound_feasible line 373
  39. theorem OAI.MatchingFPRAS.Enlargement.lifted_hole_bound line 437