OAI/SetTheory/PartitionPrinciple/Transfinite/StageTwoAssignmentSplices.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.stageTwoAssignmentLevels line 11
  2. theorem OAI.PartitionPilot.Forcing.stageTwoAssignmentCut_zero line 15
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_stageTwoAssignmentLevels line 28
  4. theorem OAI.PartitionPilot.Forcing.stageTwoAssignmentLevels_function line 50
  5. theorem OAI.PartitionPilot.Forcing.stageTwoAssignmentLevels_eq line 55
  6. theorem OAI.PartitionPilot.Forcing.stageTwoAssignmentCut_one line 76
  7. theorem OAI.PartitionPilot.Forcing.stageTwoAssignmentCut_two line 95
  8. theorem OAI.PartitionPilot.Forcing.stageTwoAssignmentCut_one_subset line 108
  9. theorem OAI.PartitionPilot.Forcing.stageTwoAssignmentCut_one_eq line 114
  10. theorem OAI.PartitionPilot.Forcing.stageTwoAssignment_upper_not_lower line 133
  11. theorem OAI.PartitionPilot.Forcing.stageTwoAssignment_upper_not_cut line 140
  12. theorem OAI.PartitionPilot.Forcing.stageTwoAssignmentSplice_upper_iff line 148
  13. theorem OAI.PartitionPilot.Forcing.stageTwoAssignment_old_no_upper line 159
  14. theorem OAI.PartitionPilot.Forcing.stageTwoAssignmentSplice_lower_eq line 164