OAI/Combinatorics/Progressions/FixedDensity/OrderedFullBoundary.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.FixedDensity.ProperPositiveOrderedSubface line 11
  2. theorem OAI.Erdos3.FixedDensity.properPositiveOrderedSubface_rank_lt_upper line 15
  3. abbrev OAI.Erdos3.FixedDensity.orderedFullLowerComplexRank line 21
  4. theorem OAI.Erdos3.FixedDensity.orderedFullLowerComplexRank_val line 35
  5. abbrev OAI.Erdos3.FixedDensity.orderedFullLowerAmbientFace line 43
  6. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_orderedFullLowerAmbientFace line 51
  7. def OAI.Erdos3.FixedDensity.orderedFullLowerConstituentPartition line 60
  8. def OAI.Erdos3.FixedDensity.orderedFullLowerPositivePartition line 73
  9. theorem OAI.Erdos3.FixedDensity.orderedFullLowerPositivePartition_le_constituent line 84
  10. theorem OAI.Erdos3.FixedDensity.orderedFullLowerPositivePartition_mono line 96
  11. def OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryPartition line 114
  12. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryPartition_le_immediate line 125
  13. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryPartition_le_constituent line 135
  14. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryPartition_mono line 147
  15. theorem OAI.Erdos3.FixedDensity.mem_orderedFullLowerBoundaryPartition_part_iff line 167
  16. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_mem_orderedFullLowerBoundaryPartition_part_iff line 190
  17. theorem OAI.Erdos3.FixedDensity.complexity_orderedFullLowerBoundaryPartition_le line 226
  18. def OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryAtomAt line 282
  19. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryAtomAt_val line 292
  20. def OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryWeight line 302
  21. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryWeight_nonneg line 313
  22. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryWeight_le_one line 322
  23. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryWeight_le_immediateWeight line 331
  24. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryWeight_sq line 361
  25. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryWeight_self line 372
  26. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryWeight_eq_one_iff line 384
  27. theorem OAI.Erdos3.FixedDensity.orderedFullLowerBoundaryWeight_eq_one_iff_all_subfaces line 402
  28. def OAI.Erdos3.FixedDensity.orderedFullLowerStructured line 421
  29. def OAI.Erdos3.FixedDensity.sourceFullMixedCoarseDensity line 430
  30. def OAI.Erdos3.FixedDensity.sourceFullMixedDefect line 438
  31. def OAI.Erdos3.FixedDensity.sourceFullMixedBoundaryWeight line 447
  32. theorem OAI.Erdos3.FixedDensity.sourceFullMixedBoundaryWeight_sq line 458
  33. theorem OAI.Erdos3.FixedDensity.sourceFullMixedBoundaryWeight_le_mixedConfigurationBoundaryIndicator line 469
  34. def OAI.Erdos3.FixedDensity.SourceFullMixedGoodAtFace line 481
  35. def OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.IsSourceFullMixedGood line 495
  36. def OAI.Erdos3.FixedDensity.sourceFullMixedLocalizedDefectSq line 505
  37. theorem OAI.Erdos3.FixedDensity.SourceFullMixedGoodAtFace.localized_defect line 515
  38. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.IsSourceFullMixedGood.localized_defect line 549