OAI/Combinatorics/CycleDecomposition/Pairing.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Batch.Pairing line 17
  2. instance OAI.ErdosGallai.Batch.Pairing.(instance at line 21) line 21
  3. instance OAI.ErdosGallai.Batch.Pairing.(instance at line 22) line 22
  4. instance OAI.ErdosGallai.Batch.Pairing.(instance at line 26) line 26
  5. theorem OAI.ErdosGallai.Batch.Pairing.apply_apply line 28
  6. theorem OAI.ErdosGallai.Batch.Pairing.apply_ne line 29
  7. def OAI.ErdosGallai.Batch.Pairing.transport line 31
  8. theorem OAI.ErdosGallai.Batch.Pairing.transport_apply line 39
  9. theorem OAI.ErdosGallai.Batch.Pairing.nonempty_of_even line 42
  10. def OAI.ErdosGallai.Batch.Pairing.oneCount line 52
  11. def OAI.ErdosGallai.Batch.Pairing.twoCount line 55
  12. theorem OAI.ErdosGallai.Batch.Pairing.oneCount_self line 59
  13. theorem OAI.ErdosGallai.Batch.Pairing.oneCount_transport line 65
  14. theorem OAI.ErdosGallai.Batch.Pairing.oneCount_eq line 71
  15. theorem OAI.ErdosGallai.Batch.Pairing.oneCount_balance line 77
  16. theorem OAI.ErdosGallai.Batch.Pairing.twoCount_transport line 92
  17. theorem OAI.ErdosGallai.Batch.Pairing.twoCount_eq line 98
  18. theorem OAI.ErdosGallai.Batch.Pairing.twoCount_forbidden line 106
  19. theorem OAI.ErdosGallai.Batch.Pairing.twoCount_balance line 123
  20. theorem OAI.ErdosGallai.Batch.Pairing.one_fraction line 157
  21. theorem OAI.ErdosGallai.Batch.Pairing.two_fraction line 173
  22. def OAI.ErdosGallai.Batch.finiteAverage line 210
  23. lemma OAI.ErdosGallai.Batch.finiteAverage_equiv line 213
  24. lemma OAI.ErdosGallai.Batch.finiteAverage_add line 218
  25. lemma OAI.ErdosGallai.Batch.finiteAverage_sum line 222
  26. lemma OAI.ErdosGallai.Batch.finiteAverage_mul_const line 227
  27. lemma OAI.ErdosGallai.Batch.finiteAverage_const line 232
  28. lemma OAI.ErdosGallai.Batch.finiteAverage_mono line 237
  29. lemma OAI.ErdosGallai.Batch.finiteAverage_prod line 242
  30. lemma OAI.ErdosGallai.Batch.exists_le_finiteAverage line 251
  31. lemma OAI.ErdosGallai.Batch.finiteAverage_indicator line 261
  32. lemma OAI.ErdosGallai.Batch.finiteAverage_pi_eval line 267
  33. lemma OAI.ErdosGallai.Batch.finiteAverage_pi_pair line 280
  34. abbrev OAI.ErdosGallai.Batch.PairingSpace line 300
  35. lemma OAI.ErdosGallai.Batch.pairingSpace_even line 302
  36. instance OAI.ErdosGallai.Batch.pairingSpace_nonempty line 307
  37. def OAI.ErdosGallai.Batch.paired line 310
  38. instance OAI.ErdosGallai.Batch.paired_decidable line 313
  39. lemma OAI.ErdosGallai.Batch.paired_ne line 316
  40. lemma OAI.ErdosGallai.Batch.paired_symm line 321
  41. lemma OAI.ErdosGallai.Batch.paired_unique line 326
  42. def OAI.ErdosGallai.Batch.pairingInvolution line 330
  43. lemma OAI.ErdosGallai.Batch.pairingInvolution_eq_or_paired line 335
  44. lemma OAI.ErdosGallai.Batch.pairingInvolution_involutive line 342
  45. lemma OAI.ErdosGallai.Batch.paired_first_moment line 353
  46. lemma OAI.ErdosGallai.Batch.paired_two_moment line 365
  47. lemma OAI.ErdosGallai.Batch.paired_first_bound line 382
  48. lemma OAI.ErdosGallai.Batch.paired_two_bound line 392
  49. lemma OAI.ErdosGallai.Batch.finiteAverage_or_le line 411
  50. lemma OAI.ErdosGallai.Batch.paired_event_local line 420
  51. lemma OAI.ErdosGallai.Batch.pairing_patterns_internal line 427
  52. lemma OAI.ErdosGallai.Batch.pairing_patterns_cross line 446
  53. lemma OAI.ErdosGallai.Batch.pairing_patterns_cross_bound line 461
  54. def OAI.ErdosGallai.Batch.Pairing.pairSetoid line 484
  55. def OAI.ErdosGallai.Batch.Pairing.PairQuotient line 500
  56. instance OAI.ErdosGallai.Batch.Pairing.(instance at line 502) line 502
  57. instance OAI.ErdosGallai.Batch.Pairing.(instance at line 507) line 507
  58. def OAI.ErdosGallai.Batch.Pairing.project line 509
  59. lemma OAI.ErdosGallai.Batch.Pairing.project_eq_iff line 511
  60. lemma OAI.ErdosGallai.Batch.Pairing.project_surjective line 514
  61. lemma OAI.ErdosGallai.Batch.Pairing.project_apply line 518
  62. lemma OAI.ErdosGallai.Batch.Pairing.fiber_card line 521
  63. lemma OAI.ErdosGallai.Batch.Pairing.card_pairQuotient line 544
  64. def OAI.ErdosGallai.Batch.oldProject line 553
  65. lemma OAI.ErdosGallai.Batch.oldProject_eq_iff line 556
  66. lemma OAI.ErdosGallai.Batch.dummy_partner_is_old line 560
  67. lemma OAI.ErdosGallai.Batch.oldProject_surjective line 574
  68. lemma OAI.ErdosGallai.Batch.old_quotient_order line 586
  69. lemma OAI.ErdosGallai.Batch.old_fiber_card_le_two line 592
  70. abbrev OAI.ErdosGallai.Batch.Outside line 612
  71. abbrev OAI.ErdosGallai.Batch.FoldDomain line 613
  72. def OAI.ErdosGallai.Batch.unfoldVertex line 615
  73. lemma OAI.ErdosGallai.Batch.unfoldVertex_bijective line 619
  74. def OAI.ErdosGallai.Batch.splitEquiv line 641
  75. abbrev OAI.ErdosGallai.Batch.FamilyQuotient line 644
  76. instance OAI.ErdosGallai.Batch.(instance at line 647) line 647
  77. instance OAI.ErdosGallai.Batch.(instance at line 652) line 652
  78. def OAI.ErdosGallai.Batch.foldOnDomain line 654
  79. def OAI.ErdosGallai.Batch.familyProject line 658
  80. lemma OAI.ErdosGallai.Batch.familyProject_surjective line 662
  81. lemma OAI.ErdosGallai.Batch.family_quotient_order_add line 671
  82. theorem OAI.ErdosGallai.Batch.family_quotient_order line 682
  83. lemma OAI.ErdosGallai.Batch.familyProject_eq_on_outside line 688
  84. lemma OAI.ErdosGallai.Batch.familyProject_eq_on_inside line 695
  85. def OAI.ErdosGallai.Batch.familyPaired line 710
  86. lemma OAI.ErdosGallai.Batch.familyProject_apply_split line 713
  87. lemma OAI.ErdosGallai.Batch.familyProject_eq_iff line 718
  88. lemma OAI.ErdosGallai.Batch.familyPaired_ne line 747
  89. lemma OAI.ErdosGallai.Batch.familyPaired_unique line 754
  90. lemma OAI.ErdosGallai.Batch.familyProject_fiber_triple line 765
  91. lemma OAI.ErdosGallai.Batch.loop_iff_familyPaired line 785
  92. lemma OAI.ErdosGallai.Batch.shared_endpoint_collision line 790
  93. lemma OAI.ErdosGallai.Batch.four_endpoint_collision line 802
  94. lemma OAI.ErdosGallai.Batch.paired_fibers_placement line 817