OAI/SetTheory/PartitionPrinciple/Transfinite/RefinementHistoryPrefixLevels.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.refinementHistoryIndices line 11
  2. theorem OAI.PartitionPilot.Forcing.mem_refinementHistoryIndices line 14
  3. theorem OAI.PartitionPilot.Forcing.refinementHistoryIndices_mono line 25
  4. def OAI.PartitionPilot.Forcing.refinementHistoryLevels line 32
  5. theorem OAI.PartitionPilot.Forcing.pair_mem_refinementHistoryLevels line 35
  6. theorem OAI.PartitionPilot.Forcing.refinementHistoryLevels_function line 55
  7. theorem OAI.PartitionPilot.Forcing.refinementHistory_fibers_disjoint line 65
  8. theorem OAI.PartitionPilot.Forcing.refinementHistoryAnchor_entry line 71
  9. theorem OAI.PartitionPilot.Forcing.refinementHistoryAnchor_function line 79
  10. def OAI.PartitionPilot.Forcing.refinementHistoryAssignmentLevels line 93
  11. theorem OAI.PartitionPilot.Forcing.mem_refinementHistoryAssignments line 97
  12. theorem OAI.PartitionPilot.Forcing.pair_mem_refinementHistoryAssignmentLevels line 111
  13. theorem OAI.PartitionPilot.Forcing.refinementHistoryAssignmentLevels_entry line 129
  14. theorem OAI.PartitionPilot.Forcing.refinementHistoryAssignmentLevels_function line 138
  15. theorem OAI.PartitionPilot.Forcing.refinementHistoryAssignmentCut_eq line 144
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryIndices_mem line 174
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryLevels_mem line 186
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryAssignmentLevels_mem line 192
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryAnchors_mem line 199
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryData line 205
  21. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_historyUnion line 235
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.historyUnion_countable_capture line 269
  23. def OAI.PartitionPilot.Forcing.refinementDataHistoryField line 330
  24. theorem OAI.PartitionPilot.Forcing.mem_refinementDataHistoryField line 335
  25. theorem OAI.PartitionPilot.Forcing.pair_mem_refinementDataHistoryField line 347
  26. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryField_entry line 359
  27. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryField_function line 371
  28. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryField_index_levels line 384
  29. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryField_domain_restrict line 397
  30. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryField_history_restrict line 413
  31. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryField_restrict line 425
  32. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryField_append line 431
  33. theorem OAI.PartitionPilot.Forcing.refinementHistoryIndices_restrict line 462
  34. theorem OAI.PartitionPilot.Forcing.refinementHistoryAssignmentCut_restrict line 475
  35. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryIndices_prefix line 486
  36. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryAssignmentCut_prefix line 493