OAI/SetTheory/PartitionPrinciple/Transfinite/InaccessibleBounds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.LinearHeightOrder.lex line 16
2. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.lexOrder line 47
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.local_assignment line 49
4. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.intervalHeights line 74
5. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.rationalUnionHeight line 92
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.rationalUnionHeight_original line 95
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.rationalUnionHeight_bounded line 98
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.rationalUnionHeight_countable line 102
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.rational_height_extension line 108
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_cardinal_bound line 131
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_cardinal_lt line 145
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.SizeBounds.countable_lt line 162
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.SizeBounds.prod_lt line 164
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.SizeBounds.sum_lt line 168
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.SizeBounds.option_lt line 172
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.SizeBounds.list_lt line 176
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.SizeBounds.sets_lt line 179
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.SizeBounds.subtype_lt line 184
19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.SizeBounds.sigma_lt line 187
20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.SizeBounds.image_cover_lt line 192