OAI/Combinatorics/UniformKServer/ActualCoordinate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Literal coordinate-key motion split into actual edits and the one mover.

  1. theorem OAI.UniformKServer.PartitionTree.diff_triangle line 19
  2. def OAI.UniformKServer.PartitionTree.pathEdits line 25
  3. def OAI.UniformKServer.PartitionTree.pathMove line 30
  4. theorem OAI.UniformKServer.PartitionTree.coordinate_split line 36
  5. theorem OAI.UniformKServer.PartitionTree.move_expect line 64