OAI/SetTheory/PartitionPrinciple/Definability/ExternalCopyRelations.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.FlatLabel line 13
2. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatVertex line 15
3. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatWord line 19
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatVertex_cover line 23
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatVertex_copy line 29
6. inductive OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.FlatStep line 36
7. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.FlatPath line 44
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.FlatPath.symm line 46
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.FlatStep.copy_eq line 50
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.FlatPath.copy_eq line 58
11. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatSetoid line 64
12. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.FlatQuotient line 69
13. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatClass line 71
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatClass_coordinate line 74
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatClass_tile line 78