OAI/Combinatorics/Progressions/FixedDensity/OrderedRegularizedCells.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.indiscreteOrderedRegularitySystem line 9
  2. theorem OAI.Erdos3.FixedDensity.indiscreteOrderedRegularitySystem_partition line 16
  3. structure OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization line 23
  4. theorem OAI.Erdos3.FixedDensity.exists_generatedOrderedPatternRegularization line 56
  5. theorem OAI.Erdos3.FixedDensity.exists_generatedOrderedPatternRegularization_before line 137
  6. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.exists_refinement_before line 217
  7. abbrev OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.BranchSystem line 363
  8. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.card_branchSystem line 373
  9. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.card_branchSystem_le line 384
  10. abbrev OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.TopAtomChoice line 403
  11. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.card_topAtomChoice line 413
  12. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.card_topAtomChoice_le line 425
  13. def OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.topAtomChoiceOf line 441
  14. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.mem_topAtomChoiceOf line 455
  15. def OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.IsInCell line 467
  16. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.mem_state_part_iff_exists_lowerGeneratorCells line 482
  17. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.same_top_atoms_iff_exists_branchSystem line 502
  18. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.regularized_edgeWeight_eq_of_mem_state_part line 537
  19. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.regularized_patternWeight_eq_of_isInCell line 557