OAI/Combinatorics/SharpRamsey/Trees/PivotExecution.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SharpLogRamsey.ActualPivot.Original line 17
  2. abbrev OAI.SharpLogRamsey.ActualPivot.Banks line 24
  3. def OAI.SharpLogRamsey.ActualPivot.banksLaw line 26
  4. lemma OAI.SharpLogRamsey.ActualPivot.banks_integral line 35
  5. def OAI.SharpLogRamsey.ActualPivot.Original.Ready line 43
  6. lemma OAI.SharpLogRamsey.ActualPivot.Original.sparse line 54
  7. def OAI.SharpLogRamsey.ActualPivot.Book.prepare line 63
  8. lemma OAI.SharpLogRamsey.ActualPivot.Book.prepare_spec line 70
  9. def OAI.SharpLogRamsey.ActualPivot.Book.choose line 77
  10. theorem OAI.SharpLogRamsey.ActualPivot.Book.ready_failure line 83
  11. theorem OAI.SharpLogRamsey.ActualPivot.Book.dual_exclusion line 91
  12. theorem OAI.SharpLogRamsey.ActualPivot.Book.primal_exclusion line 106
  13. theorem OAI.SharpLogRamsey.ActualPivot.Book.choose_caps line 121