OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainStageFromCodes.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.MeetOrderCode line 13
  2. structure OAI.PartitionPilot.Forcing.MeetFilterCode line 21
  3. def OAI.PartitionPilot.Forcing.OldMeetCode line 28
  4. structure OAI.PartitionPilot.Forcing.StrictLexHeightCode line 33
  5. theorem OAI.PartitionPilot.Forcing.birthEssential_below_earlier line 41
  6. theorem OAI.PartitionPilot.Forcing.essentialHeightDescent_of_chronological_laws line 69
  7. def OAI.PartitionPilot.Forcing.essentialBirthFiber line 90
  8. theorem OAI.PartitionPilot.Forcing.mem_essentialBirthFiber line 94
  9. theorem OAI.PartitionPilot.Forcing.essentialBirthFiber_subset line 104
  10. def OAI.PartitionPilot.Forcing.OldBridgeCode line 108
  11. theorem OAI.PartitionPilot.Forcing.birthEssentials_no_oldBridge line 114
  12. theorem OAI.PartitionPilot.Forcing.birthEssentials_same_component line 133
  13. theorem OAI.PartitionPilot.Forcing.essentialBirthFiber_same_component line 148
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.essentialBirthFiber_mem line 165
  15. structure OAI.PartitionPilot.Forcing.GroundMainStage line 193
  16. theorem OAI.PartitionPilot.Forcing.GroundMainStage.bottom_ground line 231
  17. theorem OAI.PartitionPilot.Forcing.GroundMainStage.top_ground line 232
  18. theorem OAI.PartitionPilot.Forcing.GroundMainStage.identity_ground line 233
  19. def OAI.PartitionPilot.Forcing.taggedBirth line 241
  20. theorem OAI.PartitionPilot.Forcing.pair_mem_taggedBirth line 244
  21. theorem OAI.PartitionPilot.Forcing.taggedBirth_subset line 249
  22. theorem OAI.PartitionPilot.Forcing.taggedBirth_old_iff line 252
  23. theorem OAI.PartitionPilot.Forcing.taggedBirth_fresh_iff line 257
  24. theorem OAI.PartitionPilot.Forcing.taggedBirth_function line 268
  25. theorem OAI.PartitionPilot.Forcing.taggedBirth_bound line 285
  26. theorem OAI.PartitionPilot.Forcing.taggedBirth_stamp_iff line 292
  27. theorem OAI.PartitionPilot.Forcing.taggedBirth_earlier_iff line 299
  28. def OAI.PartitionPilot.Forcing.mainStageCode line 308
  29. theorem OAI.PartitionPilot.Forcing.mainStageCode_inj line 311
  30. def OAI.PartitionPilot.Forcing.GroundMainStage.field line 326
  31. def OAI.PartitionPilot.Forcing.GroundMainStage.code line 329
  32. theorem OAI.PartitionPilot.Forcing.GroundMainStage.ext line 332
  33. theorem OAI.PartitionPilot.Forcing.GroundMainStage.field_injective line 359
  34. theorem OAI.PartitionPilot.Forcing.GroundMainStage.code_injective line 363
  35. theorem OAI.PartitionPilot.Forcing.GroundMainStage.field_ground line 367
  36. theorem OAI.PartitionPilot.Forcing.GroundMainStage.code_mem line 370
  37. def OAI.PartitionPilot.Forcing.BoundedFormula.mainStageFormula line 379
  38. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainStageFormula line 382
  39. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_mainStageFormula line 388
  40. def OAI.PartitionPilot.Forcing.GroundMainStage.ofCodes line 406