OAI/Combinatorics/SharpRamsey/Trees/PivotAlphabet.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpLogRamsey.ActualPivot.FirstSize line 17
  2. abbrev OAI.SharpLogRamsey.ActualPivot.SecondSize line 18
  3. def OAI.SharpLogRamsey.ActualPivot.firstBound line 20
  4. def OAI.SharpLogRamsey.ActualPivot.secondBound line 24
  5. abbrev OAI.SharpLogRamsey.ActualPivot.Book.LocalRaw line 32
  6. def OAI.SharpLogRamsey.ActualPivot.Book.decodeRaw line 37
  7. def OAI.SharpLogRamsey.ActualPivot.Book.allowed line 54
  8. lemma OAI.SharpLogRamsey.ActualPivot.Book.mem_allowed line 60
  9. lemma OAI.SharpLogRamsey.ActualPivot.Book.allowed_card line 69