OAI/Combinatorics/MatchingCount/Graphs/Related2.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.NumberedHierarchy.related line 14
  2. instance OAI.MatchingFPRAS.NumberedHierarchy.relatedDec line 16
  3. def OAI.MatchingFPRAS.NumberedHierarchy.component line 19
  4. lemma OAI.MatchingFPRAS.NumberedHierarchy.component_self line 21
  5. def OAI.MatchingFPRAS.NumberedHierarchy.root line 23
  6. lemma OAI.MatchingFPRAS.NumberedHierarchy.root_mem line 25
  7. lemma OAI.MatchingFPRAS.NumberedHierarchy.related_root line 27
  8. lemma OAI.MatchingFPRAS.NumberedHierarchy.cast_related line 31
  9. lemma OAI.MatchingFPRAS.NumberedHierarchy.symmetric line 41
  10. lemma OAI.MatchingFPRAS.NumberedHierarchy.triangular line 45
  11. lemma OAI.MatchingFPRAS.NumberedHierarchy.related_trans line 50
  12. lemma OAI.MatchingFPRAS.NumberedHierarchy.related_symm line 59
  13. lemma OAI.MatchingFPRAS.NumberedHierarchy.component_eq_iff line 66
  14. lemma OAI.MatchingFPRAS.NumberedHierarchy.root_eq_iff line 79
  15. lemma OAI.MatchingFPRAS.NumberedHierarchy.root_idem line 91
  16. abbrev OAI.MatchingFPRAS.NumberedHierarchy.NumberedComponent line 94
  17. def OAI.MatchingFPRAS.NumberedHierarchy.classOf line 96
  18. def OAI.MatchingFPRAS.NumberedHierarchy.quotientEquiv line 98
  19. def OAI.MatchingFPRAS.NumberedHierarchy.level line 113
  20. lemma OAI.MatchingFPRAS.NumberedHierarchy.level_cast line 116
  21. abbrev OAI.MatchingFPRAS.NumberedHierarchy.Label line 125
  22. def OAI.MatchingFPRAS.NumberedHierarchy.labelAt line 127
  23. def OAI.MatchingFPRAS.NumberedHierarchy.member line 130
  24. instance OAI.MatchingFPRAS.NumberedHierarchy.memberDec line 132
  25. lemma OAI.MatchingFPRAS.NumberedHierarchy.member_self line 135
  26. def OAI.MatchingFPRAS.NumberedHierarchy.parent line 137
  27. lemma OAI.MatchingFPRAS.NumberedHierarchy.parent_rank line 140
  28. lemma OAI.MatchingFPRAS.NumberedHierarchy.label_card_bound line 147
  29. def OAI.MatchingFPRAS.NumberedHierarchy.componentEquiv line 153
  30. def OAI.MatchingFPRAS.NumberedHierarchy.labelEquiv line 174
  31. lemma OAI.MatchingFPRAS.NumberedHierarchy.componentEquiv_mk line 178
  32. lemma OAI.MatchingFPRAS.NumberedHierarchy.labelEquiv_at line 182
  33. lemma OAI.MatchingFPRAS.NumberedHierarchy.labelEquiv_level line 186
  34. lemma OAI.MatchingFPRAS.NumberedHierarchy.member_labelAt line 190
  35. lemma OAI.MatchingFPRAS.NumberedHierarchy.member_equiv line 194
  36. lemma OAI.MatchingFPRAS.NumberedHierarchy.parent_iff line 206
  37. lemma OAI.MatchingFPRAS.NumberedHierarchy.parent_equiv_iff line 240
  38. def OAI.MatchingFPRAS.NumberedHierarchy.edgeLabel line 257
  39. def OAI.MatchingFPRAS.NumberedHierarchy.bags line 260
  40. lemma OAI.MatchingFPRAS.NumberedHierarchy.edgeLabel_equiv line 264
  41. lemma OAI.MatchingFPRAS.NumberedHierarchy.mem_bags line 272
  42. lemma OAI.MatchingFPRAS.NumberedHierarchy.bags_equiv line 277
  43. lemma OAI.MatchingFPRAS.NumberedHierarchy.bags_card_edges line 292
  44. def OAI.MatchingFPRAS.RationalSource.logicalB line 304
  45. lemma OAI.MatchingFPRAS.RationalSource.logicalB_cast line 308
  46. def OAI.MatchingFPRAS.RationalSource.height line 312
  47. lemma OAI.MatchingFPRAS.RationalSource.height_cast line 315
  48. def OAI.MatchingFPRAS.RationalSource.maxHeight line 323
  49. lemma OAI.MatchingFPRAS.RationalSource.maxHeight_cast line 325
  50. def OAI.MatchingFPRAS.RationalSource.levels line 333
  51. lemma OAI.MatchingFPRAS.RationalSource.levels_eq line 336
  52. def OAI.MatchingFPRAS.RationalSource.profile line 340
  53. lemma OAI.MatchingFPRAS.RationalSource.profile_cast line 344
  54. def OAI.MatchingFPRAS.RationalSource.pathActivity line 355
  55. lemma OAI.MatchingFPRAS.RationalSource.pathActivity_cast line 359
  56. def OAI.MatchingFPRAS.RationalSource.activity line 370
  57. lemma OAI.MatchingFPRAS.RationalSource.activity_cast line 375
  58. def OAI.MatchingFPRAS.RationalSource.realB line 390
  59. lemma OAI.MatchingFPRAS.RationalSource.realB_cast line 393
  60. lemma OAI.MatchingFPRAS.RationalSource.realB_symm line 401
  61. lemma OAI.MatchingFPRAS.RationalSource.realB_tri line 406
  62. abbrev OAI.MatchingFPRAS.RationalSource.Label line 413
  63. def OAI.MatchingFPRAS.RationalSource.bags line 415
  64. theorem OAI.MatchingFPRAS.RationalSource.label_card line 419
  65. def OAI.MatchingFPRAS.RationalSource.sourceLabelsEquiv line 433
  66. lemma OAI.MatchingFPRAS.RationalSource.bags_card_le_two line 438