OAI/SetTheory/PartitionPrinciple/Transfinite/SuccessorBirths.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.initialSegment_countable line 11
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.sequenceSup_countable line 17
3. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.sequenceSup line 31
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.lt_start line 34
5. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.upperBound line 39
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.upperBound_above line 42
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.descend_countable line 67
8. structure OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights line 95
9. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.unionHeight line 102
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.unionHeight_stage line 109
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.unionHeight_countable line 112
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.union_column_bound line 128
13. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.limitHeight line 133
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.limitHeight_stage line 138
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.limitHeight_countable line 142
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.limitHeight_top line 146
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.limitHeight_bounded line 148
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.countable_limit_height line 154
19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.stage_bound_from_top line 164
20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Heights.bounded_countable_limit line 173
21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.countable_ordinal_limit line 193
22. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.Present line 227
23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.present_nonempty line 230
24. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.birth line 232
25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.present_birth line 235
26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.birth_le_iff line 238
27. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.stageBirth line 246
28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.stageBirth_le line 248
29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.stageBirth_map line 251
30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.stageBirth_le_iff line 255
31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.born_stage_cover line 265
32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.union_born_cover line 269
33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.stageBirth_eq_iff line 272
34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.continuous_stage_no_birth line 293
35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.stageBirth_eq_of_records line 300
36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.birth_eq_of_records line 312
37. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.LocalOldMeet line 330
38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.old_meet_at line 334
39. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.union_old_meet line 358
40. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.OwnLayers line 363
41. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.laterLayer line 366
42. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.unionLayer line 371
43. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.history line 375
44. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.stages_all_filters_countable line 385
45. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.union_all_filters_countable line 390
46. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.birth line 412
47. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.birth_le line 416
48. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.birth_at_top_iff line 422
49. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.old_meet_preserved line 433
50. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.earlier_layer line 451
51. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.incoming_layer line 462
52. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.all_filters_countable line 473
53. instance OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.columnLinearOrder line 500
54. instance OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.columnWellFoundedLT line 503
55. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.descending_property line 508
56. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.rational_stages_all_filters_countable line 521
57. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.rational_union_all_filters_countable line 526
58. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.rational_bounded_all_filters_countable line 531
59. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.ordinalBirth line 548
60. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.boundedBirth line 551
61. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.ordinalBirth_lt line 554
62. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.boundedBirth_le line 557
63. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.boundedBirth_stage line 560
64. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.boundedBirth_stage_le line 563
65. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.boundedBirth_at_limit_iff line 567
66. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.ordinalBirth_old_meet line 571
67. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.boundedBirth_old_meet line 575
68. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.boundedBirth_incoming_layer line 580
69. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.countable_ordinal_chronological_limit line 585
70. def OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.NewOldMeet line 615
71. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.NewOldMeet.transport line 618
72. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Chronological.OldMeet.transport line 630
73. def OAI.PartitionPilot.Attachment.Templates.birth line 651
74. theorem OAI.PartitionPilot.Attachment.Templates.birth_le line 655
75. theorem OAI.PartitionPilot.Attachment.Templates.birth_at_step_iff line 661
76. theorem OAI.PartitionPilot.Attachment.Templates.old_meet_preserved line 672
77. theorem OAI.PartitionPilot.Attachment.Templates.new_old_meet line 676
78. def OAI.PartitionPilot.Attachment.Templates.earlier_layer line 686
79. def OAI.PartitionPilot.Attachment.Templates.incoming_layer line 698
80. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.new_old_meet line 714