OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainStageCandidates.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.MainStageLaws line 11
  2. def OAI.PartitionPilot.Forcing.MainStageValidity line 21
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.bottomFormula line 28
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_bottomFormula line 31
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.productEquationFormula line 37
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_productEquationFormula line 41
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.mainStageLawsFormula line 59
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainStageLawsFormula line 65
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.mainStageWitnessFormula line 77
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainStageWitnessFormula line 83
  11. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_mainStageWitnessFormula line 94
  12. def OAI.PartitionPilot.Forcing.SetFormula.mainStageValidityFormula line 111
  13. def OAI.PartitionPilot.Forcing.SetFormula.validMainStageCodeFormula line 119
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainStageValidityFormula line 133
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_validMainStageCodeFormula line 174
  16. theorem OAI.PartitionPilot.Forcing.GroundMainStage.validity line 191
  17. def OAI.PartitionPilot.Forcing.GroundMainStage.ofValidity line 198
  18. theorem OAI.PartitionPilot.Forcing.GroundMainStage.ofValidity_code line 212
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_mainStage_of_realize line 229
  20. def OAI.PartitionPilot.Forcing.SetFormula.mainStageCandidateFormula line 249
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainStageCandidateFormula line 259
  22. def OAI.PartitionPilot.Forcing.TransitiveGround.mainStageCandidates line 284
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_mainStageCandidates line 287
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mainStageCandidates_mem line 292
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mainStage_code_mem_candidates line 317