OAI/Combinatorics/ParityLifts/GlueTrees.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ParityWL.GlueNode line 15
  2. def OAI.ParityWL.glueNodeMap line 17
  3. def OAI.ParityWL.glueNodeParent line 20
  4. def OAI.ParityWL.glueNodeRank line 24
  5. def OAI.ParityWL.glueTree line 28
  6. lemma OAI.ParityWL.glueNodeMap_root line 44
  7. lemma OAI.ParityWL.glueNodeMap_nonroot line 47
  8. lemma OAI.ParityWL.glueTree_map_ancestor line 51
  9. lemma OAI.ParityWL.glueTree_ancestor_from_some line 60
  10. lemma OAI.ParityWL.glueTree_ancestor_nonroot line 86
  11. lemma OAI.ParityWL.RankedTree.ancestor_root_eq line 95
  12. lemma OAI.ParityWL.rooted_top_eq_root line 101
  13. lemma OAI.ParityWL.rooted_mem_ancestor line 108