OAI/SetTheory/PartitionPrinciple/Transfinite/FinalCardinality.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.factorCode line 15
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.factorCode_injective line 20
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.freeGroup_cardinal_lt line 34
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.external_cardinal_lt line 41
5. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.childCode line 53
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.childCode_injective line 58
7. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.letterCode line 69
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.letterCode_injective line 71
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.letters_cardinal_lt line 79
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.node_cardinal_lt line 85
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extension_cardinal_lt line 94
12. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.sizeCode line 109
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.sizeCode_injective line 113
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.cardinal_lt line 142
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.tasks_cardinal_lt line 155
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.internal_cardinal_lt line 159
17. def OAI.PartitionPilot.Compression.RecursiveMaps.ActionRectangle.sizeCode line 174
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.ActionRectangle.sizeCode_injective line 177
19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.ActionRectangle.cardinal_lt line 185
20. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.CardinalBound line 196
21. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.requestCode line 198
22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.requestCode_injective line 204
23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.requests_cardinal_lt line 210
24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.next_cardinal_bound line 216
25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.cardinal_lt line 234
26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.cardinal_bound_of_eq line 242
27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.initial_cardinal_bound line 245
28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.union_cardinal_bounds line 258
29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limit_cardinal_bound line 264
30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.ordinalStep_cardinal_bound line 274
31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.cardinal_eq_aleph_one line 301
32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.cardinal_lt_inaccessible line 306
33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.stage_cardinal_bound line 316
34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_cardinal_bounds line 324
35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.countableOrdinalLabels_final_cardinal_bounds line 329