OAI/SetTheory/PartitionPrinciple/Transfinite/GroundStandardInaccessible.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.InjectionCode.retarget line 14
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEmbeddable_retarget line 21
  3. theorem OAI.PartitionPilot.Forcing.ordinalSetProperty_pair_bound line 26
  4. theorem OAI.PartitionPilot.Forcing.GroundBelow.common_bound line 37
  5. theorem OAI.PartitionPilot.Forcing.GroundBelow.of_member line 45
  6. theorem OAI.PartitionPilot.Forcing.GroundCardinal.subset_of_embeddable line 67
  7. theorem OAI.PartitionPilot.Forcing.GroundCardinal.embeddable_iff_subset line 77
  8. theorem OAI.PartitionPilot.Forcing.GroundCardinal.eq_of_mutual line 87
  9. theorem OAI.PartitionPilot.Forcing.groundCardinal_iff_no_smaller_mutual line 94
  10. theorem OAI.PartitionPilot.Forcing.GroundRegular.cofinal_regular line 120
  11. theorem OAI.PartitionPilot.Forcing.GroundCofinalRegular.regular line 134
  12. theorem OAI.PartitionPilot.Forcing.GroundCofinalRegular.iff_regular line 155
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundCardinalRepresentative line 174
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundCardinalRepresentative_least line 205
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinalRelation_embeds line 226
  16. theorem OAI.PartitionPilot.Forcing.GroundStrongLimit.cardinal_strongLimit line 302
  17. theorem OAI.PartitionPilot.Forcing.GroundCardinalStrongLimit.to_groundStrongLimit line 309
  18. theorem OAI.PartitionPilot.Forcing.GroundCardinalStrongLimit.iff_groundStrongLimit line 324
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundOmegaOne_subset_of_not_countable line 351
  20. theorem OAI.PartitionPilot.Forcing.GroundInaccessibleConditions.groundOmegaOne_bound line 378
  21. theorem OAI.PartitionPilot.Forcing.GroundInaccessibleConditions.groundOmegaOne_below line 393
  22. theorem OAI.PartitionPilot.Forcing.GroundInaccessibleConditions.groundOmegaOne_mem line 403
  23. theorem OAI.PartitionPilot.Forcing.GroundStandardInaccessible.omega_mem line 434
  24. theorem OAI.PartitionPilot.Forcing.GroundStandardInaccessible.to_conditions line 446
  25. theorem OAI.PartitionPilot.Forcing.GroundInaccessibleConditions.to_standard line 456
  26. theorem OAI.PartitionPilot.Forcing.groundStandardInaccessible_iff_conditions line 467