OAI/Combinatorics/UniformKServer/PartitionTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Metric realization between occupied vertices in consecutive literal maps. Intermediate nonexistent prefixes are never used as validity witnesses.

  1. theorem OAI.UniformKServer.PartitionTree.supported_anchor_step line 19
  2. theorem OAI.UniformKServer.PartitionTree.distinct_anchor_cost line 37