OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixSelectedStepTotality.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.MainPrefixRecursionIndexCode line 12
  2. theorem OAI.PartitionPilot.Forcing.mainPrefixRecursionIndexCode_iff line 15
  3. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixRecursionIndexFormula line 25
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixRecursionIndexFormula line 37
  5. def OAI.PartitionPilot.Forcing.MainPrefixSelectedStepCode line 72
  6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_selectedStepCode line 89
  7. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixRecursionDomainFormula line 129
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixRecursionDomainFormula line 137
  9. def OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.recursionPrefixes line 151
  10. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.mem_recursionPrefixes line 154
  11. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.recursionPrefixes_ground line 159
  12. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.prefix_mem_recursionPrefixes line 185
  13. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.exists_prefix_of_mem_recursionPrefixes line 197
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_initialRecursionSeed line 233
  15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_selectedStepCode line 295
  16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitStepCode_of_fields line 360
  17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_limitStepCode line 392
  18. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.exists_limitStepCode line 430