OAI/SetTheory/PartitionPrinciple/Transfinite/MainBirthExtensions.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.ext_of_prefixes line 14
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Cone.append_prefix line 22
3. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.pastFamily line 34
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.pastCompatible line 39
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.past_glue_prefix line 47
6. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.runStep line 59
7. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.run line 68
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.run_eq line 71
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.coherent_at line 74
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.compatible line 89
11. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.diagram line 91
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.diagram_prefix line 93
13. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.before line 97
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.before_prefix line 100
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.past_glue_before line 105
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.run_generated line 117
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.stage_generated line 124
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.transition_indices line 139
19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Cone.append_leg line 144
20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transfinite.transition_generated line 158
21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.strict_top_of_transport line 174
22. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.diagram line 189
23. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.stage line 191
24. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.transition line 193
25. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.before line 196
26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.stage_zero line 198
27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.stage_successor line 201
28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.stage_limit line 204
29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.transition_self line 210
30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.transition_comp line 213
31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.strict_top line 217
32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.transition_height line 229
33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.transition_bottom line 233
34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.transition_agreement line 237
35. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.countableOrdinalLabels line 246
36. structure OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthRecord line 256
37. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthRecord.constant line 264
38. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthRecord.transport line 269
39. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthRecord.transport_back_apply line 271
40. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthRecord.successor line 276
41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthRecord.successor_original line 286
42. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthRecord.successor_source line 290
43. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.BirthCoherent line 302
44. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.unionRecordedBirth line 307
45. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.unionRecordedBirth_stage line 310
46. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.unionRecordedBirth_before line 313
47. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.unionRecordedBirth_old_meet line 319
48. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limitBirthRecord line 327
49. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limitBirthRecord_stage line 333
50. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limitBirthRecord_source line 337
51. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Cone.leg_transport line 360
52. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.ordinalStep_last_leg line 365
53. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.transition_successor line 390
54. structure OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.ConeBirth line 413
55. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.nextConeBirth line 422
56. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limitConeBirth line 438
57. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.ordinalConeBirth line 445
58. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.ConeBirth.pullback line 473
59. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.EarlierBirths line 496
60. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.EarlierCoherent line 498
61. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.birth_extension_exists line 504
62. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.extendBirths line 514
63. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.extendBirths_preserves line 517
64. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.extendBirths_source line 522