OAI/SetTheory/PartitionPrinciple/Transfinite/GroundInitialExternalChronology.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBirth_prior_layer line 34
  2. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBirth_cutoff_prior_layer line 51
  3. structure OAI.PartitionPilot.Forcing.GroundChronologicalExternal line 90
  4. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyFields_ground line 142
  5. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronology_sources_eq_below line 199
  6. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronology_old_layer line 211
  7. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronology_sources_ground_below line 231
  8. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronology_base_layer line 245
  9. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronology_finite_layers line 264
  10. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronology_union_layers line 287
  11. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronology_all_layers line 308
  12. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalMainStage line 353
  13. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalMainStage_fields line 390
  14. def OAI.PartitionPilot.Forcing.GroundChronologicalExternal.toMainStage line 433
  15. theorem OAI.PartitionPilot.Forcing.GroundChronologicalExternal.toMainStage_birth line 445
  16. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyHistory line 479
  17. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyHistory_old line 513
  18. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyHistory_stamp line 518
  19. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyHistory_limit line 526
  20. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologicalData line 549
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialExternalChronology line 610