OAI/SetTheory/PartitionPrinciple/Geometry/ExternalCopyDescent.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatTileValue line 13
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatTileValue_vertex line 18
3. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatIncidenceValue line 26
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatIncidenceValue_copy line 31
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatIncidence_stem line 38
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatIncidence_branch line 51
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatIncidence_edges line 64
8. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.toFlatQuotient line 75
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.toFlatQuotient_copy line 78
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.flatPath_iff_copy_eq line 84