OAI/Combinatorics/SharpRamsey/Windows/OpenExperiment.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.Selection.Windows.openBad line 28
  2. def OAI.SharpLogRamsey.Selection.Windows.openKeep line 32
  3. def OAI.SharpLogRamsey.Selection.Windows.openLive line 36
  4. def OAI.SharpLogRamsey.Selection.Windows.openPop line 40
  5. def OAI.SharpLogRamsey.Selection.Windows.openTargets line 49
  6. def OAI.SharpLogRamsey.Selection.Windows.openTree line 54
  7. lemma OAI.SharpLogRamsey.Selection.Windows.openPopulation_size line 60
  8. lemma OAI.SharpLogRamsey.Selection.Windows.openPopulation_length line 72
  9. theorem OAI.SharpLogRamsey.Selection.Windows.eventually_open_experiment line 79