OAI/Combinatorics/Progressions/FixedDensity/HypergraphBundleFrozenUniformity.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.positiveOrderedFaceEdge line 13
  2. theorem OAI.Erdos3.FixedDensity.positiveOrderedFaceEdge_card line 19
  3. theorem OAI.Erdos3.FixedDensity.positiveOrderedFaceEdge_nonempty line 24
  4. theorem OAI.Erdos3.FixedDensity.positiveOrderedFaceEdge_card_le line 31
  5. theorem OAI.Erdos3.FixedDensity.mem_positiveOrderedFaceEdge line 39
  6. def OAI.Erdos3.FixedDensity.positiveOrderedFaceOfEdge line 46
  7. theorem OAI.Erdos3.FixedDensity.positiveOrderedFaceEdge_ofEdge line 64
  8. theorem OAI.Erdos3.FixedDensity.positiveOrderedFaceEdge_injective line 72
  9. theorem OAI.Erdos3.FixedDensity.positiveOrderedFaceOfEdge_edge line 100
  10. abbrev OAI.Erdos3.FixedDensity.PositiveOrderedBundleEdge line 112
  11. def OAI.Erdos3.FixedDensity.positiveOrderedFaceEdgeEquiv line 115
  12. def OAI.Erdos3.FixedDensity.orderedConfigurationBaseEdges line 132
  13. theorem OAI.Erdos3.FixedDensity.empty_mem_orderedConfigurationBaseEdges line 140
  14. theorem OAI.Erdos3.FixedDensity.empty_not_mem_positiveOrderedFaceEdge_image line 145
  15. theorem OAI.Erdos3.FixedDensity.mem_orderedConfigurationBaseEdges_iff line 158
  16. def OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle line 186
  17. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_edges line 200
  18. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_projection line 207
  19. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_closed line 213
  20. def OAI.Erdos3.FixedDensity.orderedConfigurationEdgeTuple line 221
  21. theorem OAI.Erdos3.FixedDensity.positiveOrderedFaceEdge_orderIsoOfFin_val line 236
  22. def OAI.Erdos3.FixedDensity.orderedConfigurationBaseWeight line 254
  23. theorem OAI.Erdos3.FixedDensity.orderedConfigurationBaseWeight_empty line 271
  24. theorem OAI.Erdos3.FixedDensity.orderedConfigurationBaseWeight_positiveOrderedFaceEdge line 281
  25. theorem OAI.Erdos3.FixedDensity.orderedConfigurationBaseWeight_unitInterval line 376
  26. theorem OAI.Erdos3.FixedDensity.orderedConfigurationBaseWeight_idempotent line 396
  27. def OAI.Erdos3.FixedDensity.orderedConfigurationBaseDensity line 422
  28. theorem OAI.Erdos3.FixedDensity.orderedConfigurationBaseDensity_empty line 438
  29. theorem OAI.Erdos3.FixedDensity.orderedConfigurationBaseDensity_positiveOrderedFaceEdge line 447
  30. theorem OAI.Erdos3.FixedDensity.orderedConfigurationBaseDensity_unitInterval line 467
  31. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_projectedEdgeTuple line 487
  32. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_pullback_empty line 515
  33. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_pullback_positiveOrderedFaceEdge line 529
  34. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_bundleProduct line 599
  35. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_bundleCount line 640
  36. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_bundleMainProduct line 655
  37. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.projectedEdge_nonempty line 707
  38. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.projectedEdge_card_le line 716
  39. def OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBundleFace line 727
  40. def OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBundleFaceTuple line 739
  41. def OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBundleDefect line 753
  42. def OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBundleUniform line 766
  43. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBaseDensity_projectedEdge line 779
  44. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pullback_orderedConfigurationBaseWeight_decompose line 797
  45. def OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBundleLocalizedDefect line 825
  46. def OAI.Erdos3.FixedDensity.HypergraphBundle.HasOrderedConfigurationBundleLocalizedDefect line 839
  47. def OAI.Erdos3.FixedDensity.HypergraphBundle.HasOrderedConfigurationBundleFrozenUniformity line 858
  48. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.hasTaoBundleCountingStep_orderedConfiguration line 877
  49. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.exists_selectedVertex_not_mem_of_mem_erase line 1061
  50. def OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBundleFaceState line 1081
  51. def OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBundleFaceTarget line 1096
  52. def OAI.Erdos3.FixedDensity.HypergraphBundle.HasOrderedConfigurationBundleFrozenCutRepresentation line 1114
  53. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.hasOrderedConfigurationBundleFrozenUniformity_of_fullyMixed line 1141
  54. structure OAI.Erdos3.FixedDensity.HypergraphBundle.IsSourceFullBundlePreliminaryOrderedRegular line 1160
  55. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.IsSourceFullBundlePreliminaryOrderedRegular.frozenUniformity line 1169