OAI/SetTheory/PartitionPrinciple/Transfinite/GroundChronologyFieldAppend.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.isFunc_retarget_of_entries line 12
  2. theorem OAI.PartitionPilot.Forcing.GroundCompressionBirthData.union_function_successor line 26
  3. theorem OAI.PartitionPilot.Forcing.GroundCompressionBirthData.finite_function_successor line 31
  4. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.finite_birth_bound line 53
  5. theorem OAI.PartitionPilot.Forcing.GroundChronologicalHistory.prefix_birth_function_successor line 73
  6. structure OAI.PartitionPilot.Forcing.CompressionChronologyFields line 98
  7. def OAI.PartitionPilot.Forcing.GroundCompressionState.prefixFields line 116
  8. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefixFields_old line 128
  9. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefixFields_stamp line 139
  10. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefixFields_limit line 155
  11. def OAI.PartitionPilot.Forcing.GroundChronologicalHistory.restrictToCutoff line 178
  12. theorem OAI.PartitionPilot.Forcing.GroundChronologicalHistory.restrictToCutoff_values line 208
  13. def OAI.PartitionPilot.Forcing.appendHistoryValue line 223
  14. theorem OAI.PartitionPilot.Forcing.appendHistoryValue_at line 228
  15. theorem OAI.PartitionPilot.Forcing.appendHistoryValue_old line 232
  16. def OAI.PartitionPilot.Forcing.GroundChronologicalHistory.appendFixedTop line 263
  17. theorem OAI.PartitionPilot.Forcing.GroundChronologicalHistory.appendFixedTop_old line 354
  18. theorem OAI.PartitionPilot.Forcing.GroundChronologicalHistory.appendFixedTop_new line 361
  19. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefixFields_stage_laws line 387
  20. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefixFields_ground line 436
  21. def OAI.PartitionPilot.Forcing.terminalChronologyGraph line 485
  22. theorem OAI.PartitionPilot.Forcing.pair_mem_terminalChronologyGraph line 488
  23. theorem OAI.PartitionPilot.Forcing.terminalChronologyGraph_function line 493
  24. def OAI.PartitionPilot.Forcing.GroundChronologyFields.replaceTerminal line 524
  25. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.replaceTerminal_graph line 533
  26. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.replaceTerminal_value_at line 537
  27. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.replaceTerminal_value_old line 542
  28. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.replaceTerminal_value line 548
  29. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.replaceTerminal_old_entries line 557
  30. def OAI.PartitionPilot.Forcing.GroundChronologyFields.appendTime line 579
  31. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.appendTime_graph line 586
  32. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.appendTime_value_at line 590
  33. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.appendTime_old_entries line 595
  34. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.appendTime_value_old line 605
  35. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.appendTime_graph_rank_lt line 610