OAI/SetTheory/PartitionPrinciple/Geometry/ExternalHeights.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.LinearHeightOrder.first_weak line 15
2. structure OAI.PartitionPilot.Compression.RecursiveMaps.ColumnRoom line 24
3. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.heightValue line 36
4. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.extendHeight line 40
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.extendHeight_countable line 53
6. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.localHeight line 82
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.seed_column_bound line 87
8. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.gluedHeight line 91
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.gluedHeight_original line 95
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.gluedHeight_countable line 101
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.gluedHeight_column_bound line 105
12. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionHeight line 110
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionHeight_original line 114
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionHeight_countable line 118
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionHeight_top line 122
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionHeight_bounded line 125
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.external_height_extension line 131