OAI/SetTheory/PartitionPrinciple/Geometry/TileTreeGluing.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.chainIso line 13
  2. structure OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme line 24
  3. structure OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Stage line 41
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.initial line 46
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Stage.Layer line 57
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Stage.layer_nonzero line 59
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Stage.parent_present line 63
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Stage.batch line 68
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Stage.successor line 79
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Stage.successor_old line 88
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Stage.successor_new line 95
  12. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stages line 104
  13. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.chain line 108
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.vertex_coherent line 113
  15. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Node line 122
  16. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.gluedOrder line 123
  17. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.vertex line 125
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.vertex_at line 128
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.vertex_principal line 133
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.vertex_greatest_part line 137
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stage_cover line 154
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.cover line 165
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.comparison_in_vertex line 170
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.point_next line 176
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.parent_identification line 182
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.fresh_old_meet line 197
  27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.no_later_nodes_below_stage line 210
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.append_reduced_or_cancelled line 224
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.depth_zero_iff line 252
  30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.edge_root_paths line 255
  31. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.incoming line 273
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.incoming_target line 276
  33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.incoming_path line 280
  34. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.parent line 286
  35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.parent_eq line 291
  36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.parent_depth line 295
  37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.extension_nonroot line 301
  38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.incoming_of_extension line 311
  39. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.edge_is_parent line 321
  40. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.parent_root line 349
  41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.parent_of_depth_edge line 352
  42. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.parent_iff line 363
  43. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.incoming_iff line 379
  44. structure OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces line 410
  45. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.anchor line 422
  46. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.arrow line 428
  47. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.edgeInput line 436
  48. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.reindexInput line 442
  49. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.localGlue line 446
  50. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.scheme line 452
  51. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.Node line 465
  52. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.gluedOrder line 466
  53. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.vertex line 467
  54. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.vertex_principal line 470
  55. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.vertex_greatest_part line 475
  56. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.parent_identification line 481
  57. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.cover line 487
  58. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.comparison_in_vertex line 489