OAI/SetTheory/PartitionPrinciple/Geometry/GroundMainFinalSeparatedActors.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.geometry_supportBasis_mem line 16
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.decoded_supportBasis_mem line 28
3. def OAI.PartitionPilot.Forcing.TransitiveGround.decoded_supportFamily line 51
4. structure OAI.PartitionPilot.Forcing.GroundMainFinalGeometry line 70
5. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.identity_ground line 110
6. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.bottom_ground line 113
7. def OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.fields line 116
8. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.fields_ground line 122
9. def OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.code line 128
10. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.code_ground line 130
11. def OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.decodedBottom line 143
12. def OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.decodedAction line 154
13. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.decoded_order_eq line 160
14. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.decoded_action_eq line 165
15. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.decoded_supportBasis_ground line 172
16. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.decoded_unbounded line 184
17. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.decoded_countable_bound line 196
18. def OAI.PartitionPilot.Forcing.BoundedFormula.separatedActorsFormula line 218
19. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.separatedActorPairs_mem line 232