OAI/Combinatorics/UniformKServer/TreeAncestry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Literal ancestry in a finite ordered rooted tree, including all internal parks and the root.

  1. def OAI.UniformKServer.TreeAncestry.edge line 17
  2. def OAI.UniformKServer.TreeAncestry.descends line 18
  3. def OAI.UniformKServer.TreeAncestry.subtree line 19
  4. def OAI.UniformKServer.TreeAncestry.depth line 21
  5. theorem OAI.UniformKServer.TreeAncestry.depth_root line 25
  6. theorem OAI.UniformKServer.TreeAncestry.depth_child line 26
  7. theorem OAI.UniformKServer.TreeAncestry.desc_refl line 28
  8. theorem OAI.UniformKServer.TreeAncestry.desc_tail line 30
  9. theorem OAI.UniformKServer.TreeAncestry.desc_val line 33
  10. theorem OAI.UniformKServer.TreeAncestry.desc_depth line 41
  11. theorem OAI.UniformKServer.TreeAncestry.desc_same_depth line 46
  12. theorem OAI.UniformKServer.TreeAncestry.subtree_closed line 53
  13. theorem OAI.UniformKServer.TreeAncestry.subtree_boundary line 58
  14. theorem OAI.UniformKServer.TreeAncestry.subtree_total line 81
  15. def OAI.UniformKServer.TreeAncestry.ancestor line 85
  16. theorem OAI.UniformKServer.TreeAncestry.ancestor_spec line 94
  17. theorem OAI.UniformKServer.TreeAncestry.same_ancestor line 106
  18. theorem OAI.UniformKServer.TreeAncestry.ancestor_unique line 124