OAI/SetTheory/PartitionPrinciple/Definability/GroundPackedRefinementFormulaData.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.stageOneRawSingleBody line 10
  2. def OAI.PartitionPilot.Forcing.stageOneRawSingle line 27
  3. def OAI.PartitionPilot.Forcing.SetFormula.stageOneSingleBodyAt line 33
  4. def OAI.PartitionPilot.Forcing.SetFormula.stageOneSingleAt line 50
  5. theorem OAI.PartitionPilot.Forcing.map_three line 56

    Also declared: OAI/SetTheory/PartitionPrinciple/Definability/VisibilityProfileFormulas.lean:37 (same declaration text).

  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneSingleBodyAt line 64
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneSingleAt line 97
  8. def OAI.PartitionPilot.Forcing.stageOneRawCollisionBody line 116
  9. def OAI.PartitionPilot.Forcing.stageOneRawCollision line 130
  10. def OAI.PartitionPilot.Forcing.SetFormula.stageOneCollisionBodyAt line 136
  11. def OAI.PartitionPilot.Forcing.SetFormula.stageOneCollisionAt line 150
  12. theorem OAI.PartitionPilot.Forcing.map_four line 157

    Also declared: OAI/SetTheory/PartitionPrinciple/Definability/VisibilityProfileFormulas.lean:42 (same declaration text).

  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneCollisionBodyAt line 165
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneCollisionAt line 192
  15. def OAI.PartitionPilot.Forcing.stageOneRawTests line 211
  16. def OAI.PartitionPilot.Forcing.SetFormula.stageOneSinglesFormula line 221
  17. def OAI.PartitionPilot.Forcing.SetFormula.stageOneCollisionsFormula line 229
  18. def OAI.PartitionPilot.Forcing.SetFormula.stageOneTestsFormula line 239
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneSinglesFormula line 247
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneCollisionsFormula line 276
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneTestsFormula line 311
  22. def OAI.PartitionPilot.Forcing.StageTwoConditionCode line 324
  23. def OAI.PartitionPilot.Forcing.SetFormula.stageTwoConditionFormula line 332
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageTwoConditionFormula line 348
  25. def OAI.PartitionPilot.Forcing.refinementFormulaDataCode line 415
  26. theorem OAI.PartitionPilot.Forcing.refinementFormulaDataCode_injective line 418
  27. def OAI.PartitionPilot.Forcing.PackedSuccessorConditionCode line 422
  28. theorem OAI.PartitionPilot.Forcing.packedSuccessorConditionCode_code_iff line 427
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementFormulaDataCode_mem line 441
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementFormulaDataCode_fields_mem line 447
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementFormulaDataCode_mem_iff line 451
  32. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelFormulaData line 471
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelFormulaData_members line 480
  34. def OAI.PartitionPilot.Forcing.SetFormula.packedSuccessorConditionFormula line 512
  35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_packedSuccessorConditionFormula line 523
  36. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelFormulaDataCode line 568
  37. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelFormulaDataCode_mem line 571
  38. theorem OAI.PartitionPilot.Forcing.TransitiveGround.packedSuccessorConditionCode_refinementLevel_iff line 586