OAI/SetTheory/PartitionPrinciple/Forcing/GroundPreparedCertificateActionPackages.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.visibilityProfileImage_entry line 11
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.decidesVisibilityProfile_act line 42
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.forces_visibilityProfile_act line 65
4. theorem OAI.PartitionPilot.Forcing.nodeBasisImage_nonempty line 101
5. theorem OAI.PartitionPilot.Forcing.nodeBasisImage_coinitial line 108
6. theorem OAI.PartitionPilot.Forcing.nodeBasisImage_filter line 132
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.nodeBasisTransport_ground_small line 177
8. theorem OAI.PartitionPilot.Forcing.SynchronizedEnumerationCode.graph_transport line 204
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.synchronizedEnumerationTransport_ground line 290
10. theorem OAI.PartitionPilot.Forcing.nodeEnumerationImage_entry line 322
11. theorem OAI.PartitionPilot.Forcing.nodeEnumerationImage_function line 342
12. theorem OAI.PartitionPilot.Forcing.nodeEnumerationImage_onto line 354
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.nodeEnumerationImage_ground line 367
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.visibilitySupportIncidence_act_iff line 389
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparedCertificateCode_act line 436
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparedCertificateCode_act_ground_hs line 540