OAI/SetTheory/PartitionPrinciple/Definability/SeparationFulfillmentCodes.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.productRelationFormula line 13
  2. def OAI.PartitionPilot.Forcing.BoundedFormula.productFunctionFormula line 17
  3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_productRelationFormula line 23
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_productFunctionFormula line 36
  5. structure OAI.PartitionPilot.Forcing.PosetActionCode line 61
  6. def OAI.PartitionPilot.Forcing.BoundedFormula.actionOneFormula line 75
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.actionMulFormula line 78
  8. def OAI.PartitionPilot.Forcing.BoundedFormula.actionMonotoneFormula line 86
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.posetActionFormula line 94
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_posetActionFormula line 98
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_posetActionCode line 121
  12. def OAI.PartitionPilot.Forcing.SeparationActorCode line 137
  13. def OAI.PartitionPilot.Forcing.SeparationFulfillmentCode line 145
  14. def OAI.PartitionPilot.Forcing.BoundedFormula.separationActorFormula line 150
  15. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_separationActorFormula line 164
  16. def OAI.PartitionPilot.Forcing.BoundedFormula.separationFulfillmentFormula line 172
  17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_separationFulfillmentFormula line 176
  18. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_separationFulfillmentFormula line 183