OAI/Combinatorics/Progressions/FixedDensity/HypergraphBundleSourceGoodnessBridge.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.HypergraphBundle.projectedEdgeOrderIso line 17
  2. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.projectedEdgeOrderIso_apply_val line 43
  3. def OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBundleFaceTupleEquiv line 55
  4. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationBundleFaceTupleEquiv_apply line 72
  5. def OAI.Erdos3.FixedDensity.HypergraphBundle.ambientPositiveFaceOfProperSubface line 87
  6. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.ambientPositiveFaceOfProperSubface_rank line 97
  7. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.ambientPositiveFaceOfProperSubface_edge_ssubset line 103
  8. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.exists_properPositiveOrderedSubface_of_edge_ssubset line 123
  9. def OAI.Erdos3.FixedDensity.HypergraphBundle.orderedConfigurationStrictFaceFamily line 165
  10. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.mem_orderedConfigurationStrictFaceFamily line 172
  11. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.positiveOrderedFaceEdge_boundary_ssubset line 178
  12. def OAI.Erdos3.FixedDensity.HypergraphBundle.extendConfigurationFaceTuple line 204
  13. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.orderedFaceTuple_extendConfigurationFaceTuple line 214
  14. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.extendConfigurationFaceTuple_projection line 224
  15. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.sourceFullMixedBoundaryWeight_eq_strictFaceProduct line 272
  16. def OAI.Erdos3.FixedDensity.HypergraphBundle.liftProjectedSubedge line 406
  17. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.liftProjectedSubedge_subset line 414
  18. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.image_liftProjectedSubedge line 422
  19. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.liftProjectedSubedge_image_eq line 441
  20. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundaryLocalProduct_orderedConfiguration_eq_sourceFull line 464
  21. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundary_bundleCount_orderedConfiguration_eq_sourceFullMass line 683
  22. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.hasOrderedConfigurationBundleLocalizedDefect_of_sourceFullMixedGood line 786