OAI/SetTheory/PartitionPrinciple/Geometry/GroundExternalStarOverlaps.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.lowerDepthEdgeCode_iff line 11
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.parentGraph_entry line 41
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.parentGraph_eq_graph line 50
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.parentGraph_spec line 66
5. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarRoot line 89
6. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarDepth line 92
7. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarRoot_eq_encode line 120
8. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarRoot_mem line 136
9. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarDepth_eq_graph line 143
10. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarDepth_ground_function line 158
11. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarDepth_iff line 173
12. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarLayer line 188
13. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarLayers line 191
14. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarLayers_spec line 220
15. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarLayer_iff line 234
16. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarParent line 252
17. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarParent_eq_graph line 274
18. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarParent_ground_function line 288
19. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarParent_iff line 304
20. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarNonroots line 317
21. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarIncoming line 319
22. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarIncoming_ground_function line 344
23. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarIncoming_iff line 366
24. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalStarOverlaps line 400
25. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalStarFresh line 402
26. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalStarOverlapFamily line 404
27. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalStarFreshFamily line 406
28. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOverlapFresh_ground line 427
29. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOverlapFamily_spec line 437
30. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarFreshFamily_spec line 449