OAI/SetTheory/PartitionPrinciple/Transfinite/FiniteFlatHistoryCoherence.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.finiteStageHistory line 12
  2. theorem OAI.PartitionPilot.Forcing.mem_finiteStageHistory line 16
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_finiteStageHistory line 31
  4. theorem OAI.PartitionPilot.Forcing.finiteStageHistory_function line 42
  5. theorem OAI.PartitionPilot.Forcing.finiteStageHistory_restrict line 50
  6. theorem OAI.PartitionPilot.Forcing.finiteStageHistory_congr line 66
  7. theorem OAI.PartitionPilot.Forcing.flatHistoryCuts_finite_iff line 77
  8. theorem OAI.PartitionPilot.Forcing.finiteFlatCuts_down line 89
  9. theorem OAI.PartitionPilot.Forcing.finiteFlatCuts_history line 119
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteStageHistory_mem line 137
  11. def OAI.PartitionPilot.Forcing.stageThreeAssignmentLevels line 157
  12. theorem OAI.PartitionPilot.Forcing.pair_mem_stageThreeAssignmentLevels line 167
  13. theorem OAI.PartitionPilot.Forcing.stageThreeAssignmentLevels_function line 193
  14. theorem OAI.PartitionPilot.Forcing.stageThreeAssignmentLevels_eq line 198
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeIndexLevels_mem line 236
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentLevels_mem line 246
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeLevelData line 257
  18. def OAI.PartitionPilot.Forcing.threeRefinementHistory line 289
  19. theorem OAI.PartitionPilot.Forcing.pair_mem_threeRefinementHistory line 292
  20. theorem OAI.PartitionPilot.Forcing.threeRefinementHistory_function line 308
  21. theorem OAI.PartitionPilot.Forcing.threeRefinementHistory_literal line 312
  22. theorem OAI.PartitionPilot.Forcing.threeRefinementHistory_indices line 324
  23. theorem OAI.PartitionPilot.Forcing.threeRefinementHistory_levels line 348
  24. theorem OAI.PartitionPilot.Forcing.threeRefinementHistory_assignmentLevels line 353
  25. theorem OAI.PartitionPilot.Forcing.threeRefinementHistory_anchors line 359
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.threeRefinementHistory_mem line 371
  27. structure OAI.PartitionPilot.Forcing.FiniteFlatHistoryCoherence line 388