OAI/Combinatorics/MatchingCount/Graphs/HoleStrength.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Enlargement.consumed_destination_injective line 13
  2. lemma OAI.MatchingFPRAS.Enlargement.destination_nodup line 54
  3. lemma OAI.MatchingFPRAS.Enlargement.consumed_fresh line 63
  4. lemma OAI.MatchingFPRAS.Enlargement.mem_neutral_vertex_left line 75
  5. lemma OAI.MatchingFPRAS.Enlargement.mem_neutral_vertex_right line 80
  6. lemma OAI.MatchingFPRAS.Enlargement.mem_consumed_source_left line 91
  7. lemma OAI.MatchingFPRAS.Enlargement.mem_consumed_source_right line 96
  8. lemma OAI.MatchingFPRAS.Enlargement.mem_consumed_destination_right line 108
  9. lemma OAI.MatchingFPRAS.Enlargement.mem_consumed_destination_left line 116
  10. lemma OAI.MatchingFPRAS.Enlargement.internal_covered line 150
  11. theorem OAI.MatchingFPRAS.Enlargement.charged_set_eq line 158
  12. def OAI.MatchingFPRAS.Enlargement.holeStrength line 182
  13. def OAI.MatchingFPRAS.Enlargement.neutralCharge line 186
  14. def OAI.MatchingFPRAS.Enlargement.consumedCharge line 191
  15. def OAI.MatchingFPRAS.Enlargement.totalDeletionCharge line 197
  16. theorem OAI.MatchingFPRAS.Enlargement.deletion_charge_trace line 202
  17. theorem OAI.MatchingFPRAS.Enlargement.deletion_capacity_bound line 290
  18. def OAI.MatchingFPRAS.Enlargement.blockCharge line 322
  19. lemma OAI.MatchingFPRAS.Enlargement.blockCharge_potential line 327
  20. def OAI.MatchingFPRAS.Enlargement.pathConstant line 365
  21. lemma OAI.MatchingFPRAS.Enlargement.forcing_weight_charge line 368