OAI/Combinatorics/UniformKServer/TreeTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The laminar cuts of the literal finite tree; exact matching transport and an occupied-endpoint separating edge below a deepest common ancestor.

  1. theorem OAI.UniformKServer.TreeAncestry.comparable_depth line 18
  2. theorem OAI.UniformKServer.TreeAncestry.subtree_laminar line 24
  3. def OAI.UniformKServer.TreeAncestry.pathCost line 42
  4. theorem OAI.UniformKServer.TreeAncestry.matching line 46
  5. theorem OAI.UniformKServer.TreeAncestry.separating_edge line 62
  6. theorem OAI.UniformKServer.TreeAncestry.edge_le_path line 95