OAI/Combinatorics/SharpRamsey/Trees/ChronologicalTree.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.ChronologicalTree.balanced line 10
  2. def OAI.SharpLogRamsey.ChronologicalTree.inorder line 19
  3. lemma OAI.SharpLogRamsey.ChronologicalTree.inorder_length line 23
  4. lemma OAI.SharpLogRamsey.ChronologicalTree.balanced_card line 29
  5. lemma OAI.SharpLogRamsey.ChronologicalTree.balanced_height line 41
  6. lemma OAI.SharpLogRamsey.ChronologicalTree.balanced_interval line 62
  7. def OAI.SharpLogRamsey.ChronologicalTree.Chronological line 78
  8. lemma OAI.SharpLogRamsey.ChronologicalTree.balanced_chronological line 83
  9. lemma OAI.SharpLogRamsey.ChronologicalTree.inorder_pairwise line 99
  10. lemma OAI.SharpLogRamsey.ChronologicalTree.balanced_nodup line 113