OAI/SetTheory/PartitionPrinciple/Geometry/GroundDefinableSelections.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.SetFormula.partialCollectionFormula line 9
  2. def OAI.PartitionPilot.Forcing.SetFormula.relationImageFormula line 12
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_partialCollectionFormula line 23
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_relationImageFormula line 31
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.partialCollection_witness line 42
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.definable_image_mem line 62
  7. def OAI.PartitionPilot.Forcing.SetFormula.separationCodeFormula line 97
  8. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_separation line 108