OAI/SetTheory/PartitionPrinciple/Transfinite/GluingBirthRanges.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.batchBirth line 16
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.batch_new_old_meet line 20
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.batch_old_meet_preserved line 25
4. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.batch_earlier_layer line 30
5. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.batch_incoming_layer line 37
6. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.recordedStageBirth line 57
7. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.recordedUnionBirth line 62
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.recordedBirth_stage line 66
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.recordedBirth_original line 76
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.recordedBirth_next line 79
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.recordedBirth_cases line 83
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.recordedStageBirth_lt_later line 95
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.recordedStageBirth_old_meet line 105
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.recordedUnionBirth_old_meet line 119
15. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepBirth line 138
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepBirth_iso line 143
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepBirth_old line 152
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepBirth_le line 159
19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.step_new_old_meet line 164
20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.step_old_meet_preserved line 171
21. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.step_earlier_layer line 179
22. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.step_incoming_layer line 189
23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.step_no_birth line 201
24. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.vertex line 222
25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.vertex_cover line 226
26. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.incoming_layer line 231
27. instance OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.child_countable line 251
28. instance OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.child_countable line 259
29. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.tile_incoming_layer line 261
30. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.orderedBirth line 281
31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordered_birth_preserves line 289
32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordered_new_old_meet line 300
33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordered_old_meet_preserved line 309
34. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordered_earlier_layer line 319
35. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordered_incoming_layer line 331
36. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.recordBirth line 372
37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.different_fresh_meet line 376
38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.record_old_meet line 383
39. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageBirth line 420
40. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageBirth_next line 425
41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageBirth_up line 428
42. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.unionBirth line 434
43. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.unionBirth_stage line 441
44. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.unionBirth_original line 444
45. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialBirth line 449
46. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialBirth_global line 452
47. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialBirth_inclusion line 455
48. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialBirth_later line 460
49. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialBirth_step_iso line 466
50. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialBirth_step line 473
51. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageBirth_lt_later line 490
52. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialBirth_before line 501
53. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageBirth_old_meet line 510
54. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.unionBirth_old_meet line 524
55. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.partialBirth_old_meet line 531
56. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.externalBirth line 554
57. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffBirth line 556
58. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.externalBirth_original line 559
59. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffBirth_global line 564
60. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffBirth_ordered line 568
61. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffBirth_before line 582
62. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.externalBirth_old_meet line 588
63. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffBirth_old_meet line 593
64. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffBirth_new_old_meet line 599
65. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.cutoffBirth_incoming_layer line 608
66. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageBirth_cases line 630
67. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.unionBirth_cases line 643
68. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.externalBirth_cases line 660