OAI/Combinatorics/MatchingCount/Graphs/Related.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Enlargement.edge_activity_le_realBottleneck line 13
  2. theorem OAI.MatchingFPRAS.Enlargement.realBottleneck_noncentral_edge line 24
  3. theorem OAI.MatchingFPRAS.Enlargement.realBottleneck_central_edge line 53
  4. theorem OAI.MatchingFPRAS.Enlargement.source_effective_profile line 101
  5. theorem OAI.MatchingFPRAS.Enlargement.effective_profile_incident_near line 122
  6. theorem OAI.MatchingFPRAS.Hierarchy.acyclic_of_unique_lower line 187
  7. def OAI.MatchingFPRAS.Hierarchy.Related line 216
  8. lemma OAI.MatchingFPRAS.Hierarchy.related_symm line 220
  9. lemma OAI.MatchingFPRAS.Hierarchy.related_trans line 227
  10. def OAI.MatchingFPRAS.Hierarchy.thresholdSetoid line 241
  11. abbrev OAI.MatchingFPRAS.Hierarchy.Component line 245
  12. abbrev OAI.MatchingFPRAS.Hierarchy.Label line 247
  13. def OAI.MatchingFPRAS.Hierarchy.labelAt line 249
  14. def OAI.MatchingFPRAS.Hierarchy.Mem line 252
  15. lemma OAI.MatchingFPRAS.Hierarchy.mem_labelAt line 255
  16. lemma OAI.MatchingFPRAS.Hierarchy.mem_class_iff line 258
  17. lemma OAI.MatchingFPRAS.Hierarchy.exists_mem line 263
  18. lemma OAI.MatchingFPRAS.Hierarchy.eq_of_level_of_mem line 267
  19. lemma OAI.MatchingFPRAS.Hierarchy.related_of_mem line 278
  20. lemma OAI.MatchingFPRAS.Hierarchy.mem_of_related line 283
  21. lemma OAI.MatchingFPRAS.Hierarchy.related_mono line 288
  22. def OAI.MatchingFPRAS.Hierarchy.Parent line 291
  23. def OAI.MatchingFPRAS.Hierarchy.tree line 294
  24. lemma OAI.MatchingFPRAS.Hierarchy.parent_mem line 300
  25. lemma OAI.MatchingFPRAS.Hierarchy.parent_unique line 308
  26. theorem OAI.MatchingFPRAS.Hierarchy.tree_acyclic line 319
  27. lemma OAI.MatchingFPRAS.Hierarchy.parent_exists line 335
  28. lemma OAI.MatchingFPRAS.Hierarchy.level_zero_unique line 345
  29. lemma OAI.MatchingFPRAS.Hierarchy.reaches_level_zero line 354
  30. theorem OAI.MatchingFPRAS.Hierarchy.tree_connected line 366
  31. instance OAI.MatchingFPRAS.Hierarchy.labelFintype line 377
  32. theorem OAI.MatchingFPRAS.Hierarchy.label_card_le line 379
  33. def OAI.MatchingFPRAS.Hierarchy.dyadicLevel line 387
  34. lemma OAI.MatchingFPRAS.Hierarchy.dyadic_lower line 392
  35. lemma OAI.MatchingFPRAS.Hierarchy.dyadic_upper line 397
  36. lemma OAI.MatchingFPRAS.Hierarchy.dyadic_near line 410
  37. lemma OAI.MatchingFPRAS.Hierarchy.dyadic_upper_of_lt line 420
  38. lemma OAI.MatchingFPRAS.Hierarchy.dyadic_near_of_lt line 431
  39. lemma OAI.MatchingFPRAS.Hierarchy.common_vertex_adjacent line 442
  40. lemma OAI.MatchingFPRAS.Hierarchy.memberships_card_le_two line 452
  41. def OAI.MatchingFPRAS.Hierarchy.Incident line 476
  42. def OAI.MatchingFPRAS.Hierarchy.edgeLabel line 478
  43. def OAI.MatchingFPRAS.Hierarchy.memberships line 481
  44. lemma OAI.MatchingFPRAS.Hierarchy.mem_memberships line 487
  45. lemma OAI.MatchingFPRAS.Hierarchy.incident_mem_label line 495
  46. lemma OAI.MatchingFPRAS.Hierarchy.membership_mem line 504
  47. lemma OAI.MatchingFPRAS.Hierarchy.memberships_level_near line 516
  48. theorem OAI.MatchingFPRAS.Hierarchy.memberships_tree_bags line 526
  49. lemma OAI.MatchingFPRAS.Hierarchy.membership_count line 538
  50. lemma OAI.MatchingFPRAS.Hierarchy.common_height_le line 546
  51. lemma OAI.MatchingFPRAS.Hierarchy.edge_strength_lt_twice_height line 555
  52. lemma OAI.MatchingFPRAS.Hierarchy.adjacent_heights line 560