OAI/Combinatorics/Progressions/FixedDensity/HypergraphBundleFiltration.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.FixedDensity.HypergraphBundle.DoubledOccurrenceVertex line 17
  2. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledVertexForget line 20
  3. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledVertexLift line 26
  4. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledVertexForget_lift line 35
  5. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledVertexLift_injective line 42
  6. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledAssignment line 50
  7. def OAI.Erdos3.FixedDensity.HypergraphBundle.splitDoubledAssignmentEquiv line 60
  8. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.splitDoubledAssignmentEquiv_symm_apply line 82
  9. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.mean_splitDoubledAssignment line 91
  10. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledAssignment_lift_false line 130
  11. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledAssignment_lift_true line 159
  12. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdge line 187
  13. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.mem_doubledEdge line 192
  14. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.image_forget_doubledEdge line 200
  15. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_doubledEdge line 220
  16. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdge_copy_independent_of_subset line 227
  17. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdge_false_ne_true_of_mem_complement line 237
  18. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdge_false_eq_true_iff_subset line 257
  19. abbrev OAI.Erdos3.FixedDensity.HypergraphBundle.DoubledEdgeSource line 272
  20. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdgeOfSource line 276
  21. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledSourceProduct line 282
  22. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledSourceProduct_doubledAssignment line 291
  23. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledRemainderMoment_eq_mean_doubledSourceProduct line 364
  24. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdges line 375
  25. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdgeOfSource_mem_doubledEdges line 380
  26. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.mem_doubledEdges_iff line 389
  27. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledProjection line 407
  28. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledProjection_lift line 413
  29. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.image_doubledProjection_doubledEdge line 422
  30. def OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside line 444
  31. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_edges line 470
  32. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_projection line 477
  33. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_edge_card line 483
  34. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_order_le_eraseEdge line 493
  35. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_order_le line 505
  36. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_doubledEdges_le line 511
  37. def OAI.Erdos3.FixedDensity.HypergraphBundle.RemainingEdgesMeetComplement line 525
  38. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdgeOfSource_injective line 530
  39. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdgeSourceEquiv line 566
  40. def OAI.Erdos3.FixedDensity.HypergraphBundle.sourceOfDoubledEdge line 590
  41. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdgeOfSource_sourceOfDoubledEdge line 599
  42. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.sourceOfDoubledEdge_doubledEdgeOfSource line 611
  43. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_doubledEdges_eq line 622
  44. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdge_image_forget_of_subset line 632
  45. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_closed line 665
  46. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_closed_of_maximal line 694
  47. def OAI.Erdos3.FixedDensity.HypergraphBundle.filterEdges line 722
  48. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.filterEdges_edges line 738
  49. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.mem_filterEdges_edges line 745
  50. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.filterEdges_projection line 754
  51. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.filterEdges_order_le line 760
  52. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_filterEdges_edges_le line 770
  53. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.filterEdges_closed line 776
  54. def OAI.Erdos3.FixedDensity.HypergraphBundle.lowerOrder line 788
  55. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.lowerOrder_edges line 794
  56. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.mem_lowerOrder_edges line 801
  57. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.lowerOrder_order_lt line 808
  58. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.lowerOrder_order_le line 817
  59. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_lowerOrder_edges_le line 822
  60. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.lowerOrder_closed line 827
  61. def OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundary line 836
  62. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundary_edges line 842
  63. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.mem_strictBoundary_edges line 849
  64. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundary_order_le line 856
  65. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundary_order_lt line 861
  66. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_strictBoundary_edges_le line 870
  67. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundary_closed line 875
  68. def OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct line 884
  69. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct_filterEdges line 890
  70. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct_lowerOrder line 900
  71. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct_strictBoundary line 909
  72. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct_filter_mul_filter_not line 917
  73. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct_eraseEdge_mul line 930
  74. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdge_injective line 942
  75. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdges_eq_image_union line 951
  76. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.image_true_sdiff_image_false line 978
  77. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.prod_image_doubledEdge_main line 1023
  78. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct_duplicateOutside line 1036
  79. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct_duplicateOutside_lowerOrder line 1103