OAI/SetTheory/PartitionPrinciple/Forcing/GroundRepresentedDomainConditions.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.SetFormula.stageOneForcingFormula line 15
  2. def OAI.PartitionPilot.Forcing.SetFormula.stageOneForcingAt line 19
  3. def OAI.PartitionPilot.Forcing.SetFormula.stageOneClassAt line 23
  4. def OAI.PartitionPilot.Forcing.stageOneRawForces line 29
  5. def OAI.PartitionPilot.Forcing.stageOneRawClass line 33
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneForcingAt line 40
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneClassAt line 47
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneRawForces_iff line 56
  9. def OAI.PartitionPilot.Forcing.PreparationForcingCode line 79
  10. def OAI.PartitionPilot.Forcing.SetFormula.preparationForcingFormula line 89
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_preparationForcingFormula line 108
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneRawForces_condition_mono line 143
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rawForces_pair_condition_mono line 155
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationForcingCode_condition_mono line 170
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationForcingCode_nice_condition_mono line 205
  16. def OAI.PartitionPilot.Forcing.TransitiveGround.representedReuseFormula line 240
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_representedReuseFormula line 251
  18. def OAI.PartitionPilot.Forcing.TransitiveGround.representedEntryFormula line 300
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_representedEntryFormula line 313
  20. def OAI.PartitionPilot.Forcing.TransitiveGround.representedDomainConditions line 371
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.representedDomainConditions_subset line 380
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.representedParams_ground line 395
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.representedDomainConditions_mem line 411
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_representedDomainConditions line 421