OAI/Combinatorics/SharpRamsey/Windows/GoodPopulation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.FreshExecution.population_flatMap line 10
  2. abbrev OAI.SharpLogRamsey.Selection.Windows.goodMiddle line 27
  3. def OAI.SharpLogRamsey.Selection.Windows.goodTarget line 31
  4. lemma OAI.SharpLogRamsey.Selection.Windows.goodTarget_eq line 40
  5. lemma OAI.SharpLogRamsey.Selection.Windows.goodTarget_not_bad line 46
  6. lemma OAI.SharpLogRamsey.Selection.Windows.goodTarget_before line 52
  7. lemma OAI.SharpLogRamsey.Selection.Windows.goodTarget_before_next line 62
  8. theorem OAI.SharpLogRamsey.Selection.Windows.goodPopulation_pairwise line 71
  9. lemma OAI.SharpLogRamsey.Selection.Windows.goodPopulation_length line 89
  10. lemma OAI.SharpLogRamsey.Selection.Windows.goodMiddle_card line 100
  11. lemma OAI.SharpLogRamsey.Selection.Windows.goodPopulation_size line 118
  12. lemma OAI.SharpLogRamsey.Selection.Windows.goodPopulation_predeletion line 129