OAI/SetTheory/PartitionPrinciple/Geometry/OutwardSchedule.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Partial line 13
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialOrder line 15
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialEmbedding line 18
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialEmbedding_old line 22
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialEmbedding_tile line 26
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialOldVertex line 33
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialOldVertex_global line 37
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partial_no_later_nodes line 46
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialLater line 51
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialLater_global line 57
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partial_cover line 64
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partial_outside_meet line 69
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partial_new_vertex_meet line 86
  14. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.FullRight line 113
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.fullRight_reindex line 116
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.edge_full_at_old line 132
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.old_local_full line 146
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.old_layer_no_fresh line 156
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.fresh_layer_is_tile line 164
  20. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.Layer line 170
  21. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.Cutoff line 171
  22. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffOrder line 172
  23. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffEmbedding line 174
  24. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffPlacedTile line 178
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffPlacedTile_global line 184
  26. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffTileRoot line 192
  27. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffTileChild line 198
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffTileRoot_global line 204
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffTileChild_global line 212
  30. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.chosenWellOrder line 228
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.chosenWellOrder_wf line 231
  32. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.layerBefore line 238
  33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.layerBefore_irrefl line 242
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.layerBefore_wf line 246
  35. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Position line 251
  36. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.positionBefore line 253
  37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.positionBefore_wf line 256
  38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.parent_position_before line 259
  39. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.orderedAttachment line 269
  40. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.orderedCutoffEmbedding line 275
  41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.ordered_limit line 279
  42. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.ordered_layer_cover line 288
  43. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.ordered_new_vertex_meet line 296