OAI/SetTheory/PartitionPrinciple/Transfinite/FinalStageBounds.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.birthStep line 10
2. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.birthRun line 17
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.birthRun_eq line 20
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.birthRun_coherent_at line 23
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.birthRun_earlier_coherent line 42
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.birthRun_generated line 46
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.birthRun_source line 53
8. structure OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.BoundedBirthCertificate line 69
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.BoundedBirthCertificate.fiber_basis line 78
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.BoundedBirthCertificate.all_filters_countable line 91
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.BoundedBirthCertificate.localizes line 99
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.birthRun_origin line 110
13. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalBirth line 126
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalBirth_stage line 130
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalBirth_old_meet line 133
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalBirth_origin line 139
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalBirth_main_le line 144
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalBirth_main_eq_canonical line 148
19. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalBirthCertificate line 159
20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_all_filters_countable line 165
21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_filter_basis line 168
22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_filters_localized line 171
23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.countableOrdinalLabels_final_filter_basis line 174
24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_countable_upper_bound line 185
25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.countable_actors_in_stage line 193
26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.countable_data_in_stage line 206