OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainSuccessorProfilePreservation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.external_cutoff_strict line 57
  2. def OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.externalTransition line 61
  3. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.externalTransition_graphs line 90
  4. structure OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData line 105
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialMainSuccessor line 187
  6. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_rank_lt_of_components line 268
  7. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compression_union_rank_lt line 293
  8. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_rank_lt line 298
  9. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_code_rank_lt line 309
  10. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_code_rank_lt_omegaOne line 318
  11. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.transition_code_rank_lt line 329
  12. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compression_limit_mem line 353
  13. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.external_limit_mem line 357
  14. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_cutoff_mem line 363
  15. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_time_domain_mem line 367
  16. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_birth_rank_lt line 371
  17. theorem OAI.PartitionPilot.Forcing.GroundCompressionBirthData.prior_entry line 389
  18. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.originalFiber_image line 409
  19. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.boundedOriginalFiber_image line 420
  20. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.oldBirthFiberCoverage line 438
  21. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.coversOldBirths line 445
  22. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.capProfile_preserved line 458