OAI/SetTheory/PartitionPrinciple/Transfinite/GroundStructuralHistoryTestUnions.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory line 13
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_structuralRefinementHistory line 21
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_structuralRefinementHistory line 49
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory_entry line 63
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory_domain_restrict line 87
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory_history_restrict line 104
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory_append line 116
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory_function line 141
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.refinementDataHistoryFieldFormula line 169
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_refinementDataHistoryFieldFormula line 175
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementDataHistoryField_mem line 197
  12. structure OAI.PartitionPilot.Forcing.RefinementDataHistory line 227
  13. def OAI.PartitionPilot.Forcing.refinementDataHistoryIndices line 236
  14. def OAI.PartitionPilot.Forcing.refinementDataHistoryLevels line 239
  15. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.index_function line 246
  16. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.index_literal line 249
  17. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.levels_function line 253
  18. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.coverage line 258
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementDataHistoryIndices_mem line 270
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementDataHistoryLevels_mem line 279
  21. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.restrict line 297
  22. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.append line 307
  23. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.prefix_cut line 328
  24. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.assignment_level_iff line 346
  25. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.rawTests_splice_below line 356
  26. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.rawTests_splice_above line 369
  27. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.rawTests_on_earlier_cut line 383
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rawRefinementFormulaData_level line 402
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory_decoded line 411
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory_fields line 417
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory_structural_fields line 426
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralRefinementHistory_dataHistory line 435
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralHistory_rawTests_union line 470