OAI/SetTheory/PartitionPrinciple/Transfinite/GroundInitialMainStage.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroundMainStage.initialBirth line 15
2. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialBirth_function line 18
3. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialBirth_entry line 22
4. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialBirth_ground line 26
5. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialBirth_old_meet line 34
6. def OAI.PartitionPilot.Forcing.GroundMainStage.initialHistory line 40
7. def OAI.PartitionPilot.Forcing.GroundMainStage.initialChronological line 68
8. def OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyField line 84
9. def OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyGraph line 88
10. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyGraph_entry line 92
11. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyGraphs_ground line 99
12. def OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyBound line 122
13. theorem OAI.PartitionPilot.Forcing.GroundMainStage.mem_initialChronologyBound line 125
14. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyBound_ground line 134
15. def OAI.PartitionPilot.Forcing.GroundMainStage.initialGroundChronologyFields line 140
16. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialGroundChronologyFields_graph line 159
17. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialGroundChronologyFields_value line 163
18. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialGroundChronologyFields_values line 171
19. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialGroundChronologyFields_code_ground line 182
20. theorem OAI.PartitionPilot.Forcing.InitialMainAlgebra.carrier_eq_pair line 192
21. def OAI.PartitionPilot.Forcing.TransitiveGround.initialMainStage line 209
22. def OAI.PartitionPilot.Forcing.TransitiveGround.initialMainChronological line 236
23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.initialMainStage_fields line 240
24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.initialMainChronological_fields line 247
25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.initialMainStage_two_points line 253
26. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyCore line 272
27. def OAI.PartitionPilot.Forcing.GroundMainStage.initialDecodedChronology line 289
28. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialDecodedChronology_values line 302
29. def OAI.PartitionPilot.Forcing.GroundMainStage.initialSerializedChronology line 328
30. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialSerializedChronology_layers line 355
31. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialSerializedChronology_layerWitness line 360
32. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialSerializedChronology_values line 369
33. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialSerializedChronology_code_ground line 381
34. theorem OAI.PartitionPilot.Forcing.GroundMainStage.exists_initialSerializedChronology line 386
35. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyField_rank_lt line 412
36. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyBound_rank_lt line 421
37. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialChronologyGraph_rank_lt line 424
38. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialSerializedChronology_code_rank_lt line 434
39. theorem OAI.PartitionPilot.Forcing.GroundMainStage.initialSerializedChronology_code_rank_lt_inaccessible line 453