OAI/SetTheory/PartitionPrinciple/Transfinite/GroundSerializedChronologyTimeEquality.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internal_chronological_coinitiality line 16
  2. structure OAI.PartitionPilot.Forcing.ChronologyPointCode line 53
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.chronologyPointFormula line 62
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_chronologyPointFormula line 67
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_chronologyPointFormula line 84
  6. structure OAI.PartitionPilot.Forcing.GroundChronologicalHistory line 99
  7. theorem OAI.PartitionPilot.Forcing.GroundChronologicalHistory.all_filters_internal_countable line 125
  8. theorem OAI.PartitionPilot.Forcing.GroundChronologicalHistory.exists_internal_basis line 166
  9. structure OAI.PartitionPilot.Forcing.ChronologyCoreCode line 190
  10. def OAI.PartitionPilot.Forcing.BoundedFormula.chronologyFunctionsFormula line 200
  11. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_chronologyFunctionsFormula line 205
  12. def OAI.PartitionPilot.Forcing.BoundedFormula.chronologyPointsFormula line 214
  13. def OAI.PartitionPilot.Forcing.BoundedFormula.chronologyCoreFormula line 227
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_chronologyCoreFormula line 231
  15. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_chronologyCoreFormula line 250
  16. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.decoded_point line 265
  17. def OAI.PartitionPilot.Forcing.GroundChronologyFields.toHistory line 271
  18. def OAI.PartitionPilot.Forcing.GroundChronologicalHistory.of_inclusion line 305
  19. theorem OAI.PartitionPilot.Forcing.GroundChronologicalHistory.exists_extension_basis line 323
  20. def OAI.PartitionPilot.Forcing.GroundChronologyFields.attainedBound line 351
  21. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.mem_attainedBound line 354
  22. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.attainedBound_ground line 371
  23. def OAI.PartitionPilot.Forcing.GroundChronologyFields.normalizeBound line 376
  24. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.normalizeBound_graph line 389
  25. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.normalizeBound_value line 392
  26. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.normalizeBound_core line 395
  27. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.attainedBound_rank_lt line 403
  28. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.normalizeBound_code_rank_lt line 408
  29. theorem OAI.PartitionPilot.Forcing.ChronologyPointCode.retarget_time line 423
  30. def OAI.PartitionPilot.Forcing.GroundChronologyFields.restrictTo line 442
  31. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.restrictTo_value line 456
  32. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.restrictTo_graph line 461
  33. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.restrictTo_core line 464
  34. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.restrictTo_code_ground line 475
  35. structure OAI.PartitionPilot.Forcing.GroundSerializedChronology line 486
  36. def OAI.PartitionPilot.Forcing.GroundSerializedChronology.layerWitness line 504
  37. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.layerWitness_entry line 508
  38. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.layerWitness_ground line 515
  39. def OAI.PartitionPilot.Forcing.GroundSerializedChronology.decodedLayer line 519
  40. def OAI.PartitionPilot.Forcing.GroundSerializedChronology.toHistory line 531
  41. def OAI.PartitionPilot.Forcing.GroundSerializedChronology.codeFields line 534
  42. def OAI.PartitionPilot.Forcing.GroundSerializedChronology.code line 537
  43. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.code_ground line 539
  44. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.toHistory_values line 545
  45. def OAI.PartitionPilot.Forcing.GroundSerializedChronology.castTime line 562
  46. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.castTime_code line 564
  47. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.castTime_graph line 568
  48. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.castTime_value line 573
  49. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.castTime_layers line 578