OAI/SetTheory/PartitionPrinciple/Forcing/GroundStoredPreparedFamilyActions.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.certificateUsedSupports line 11
  2. theorem OAI.PartitionPilot.Forcing.mem_certificateUsedSupports line 15
  3. def OAI.PartitionPilot.Forcing.preparationEventUsedSupports line 20
  4. theorem OAI.PartitionPilot.Forcing.preparationEventUsedSupports_active line 25
  5. theorem OAI.PartitionPilot.Forcing.preparationEventUsedSupports_idle line 42
  6. def OAI.PartitionPilot.Forcing.BoundedFormula.certificateBasisMemberFormula line 59
  7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_certificateBasisMemberFormula line 62
  8. def OAI.PartitionPilot.Forcing.BoundedFormula.preparationEventSupportFormula line 74
  9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_preparationEventSupportFormula line 78
  10. def OAI.PartitionPilot.Forcing.preparationTupleCode line 100
  11. def OAI.PartitionPilot.Forcing.tupleImageWithOmega line 103
  12. def OAI.PartitionPilot.Forcing.preparationTupleImage line 110
  13. def OAI.PartitionPilot.Forcing.preparationTupleActionGraph line 114
  14. theorem OAI.PartitionPilot.Forcing.pair_mem_preparationTupleActionGraph line 120
  15. def OAI.PartitionPilot.Forcing.TransitiveGround.pairDefinition line 142
  16. def OAI.PartitionPilot.Forcing.TransitiveGround.imageDefinition line 148
  17. def OAI.PartitionPilot.Forcing.TransitiveGround.converseDefinition line 158
  18. def OAI.PartitionPilot.Forcing.TransitiveGround.composeDefinition line 172
  19. def OAI.PartitionPilot.Forcing.TransitiveGround.actionPairDefinition line 187
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationTupleActionGraph_mem line 205
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationTupleImage_mem_bound line 284
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationTupleActionGraph_function line 330
  23. theorem OAI.PartitionPilot.Forcing.preparationFamilyFirst_usedSupports_image line 383
  24. theorem OAI.PartitionPilot.Forcing.preparationFamilyFirst_usedSupports_subset line 438
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparedCertificateFamily_act line 472
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparedCertificateFamily_act_support line 580
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.storedPreparationFamily_structural_act_support line 665