OAI/SetTheory/PartitionPrinciple/Geometry/AssignmentNestedSplices.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.assignmentCut line 10
  2. def OAI.PartitionPilot.Forcing.assignmentUpper line 13
  3. def OAI.PartitionPilot.Forcing.assignmentSplice line 16
  4. theorem OAI.PartitionPilot.Forcing.mem_assignmentCut line 19
  5. theorem OAI.PartitionPilot.Forcing.mem_assignmentUpper line 24
  6. theorem OAI.PartitionPilot.Forcing.mem_assignmentSplice line 34
  7. theorem OAI.PartitionPilot.Forcing.assignmentCut_subset line 40
  8. theorem OAI.PartitionPilot.Forcing.assignmentUpper_subset line 44
  9. theorem OAI.PartitionPilot.Forcing.assignmentSplice_subset line 48
  10. theorem OAI.PartitionPilot.Forcing.assignmentCut_mono line 55
  11. theorem OAI.PartitionPilot.Forcing.assignmentCut_nested line 61
  12. theorem OAI.PartitionPilot.Forcing.assignmentCut_eq_of_lower line 74
  13. theorem OAI.PartitionPilot.Forcing.assignmentCut_full line 82
  14. theorem OAI.PartitionPilot.Forcing.assignmentCut_splice line 90
  15. theorem OAI.PartitionPilot.Forcing.assignmentUpper_splice line 103
  16. theorem OAI.PartitionPilot.Forcing.assignmentSplice_self line 116
  17. theorem OAI.PartitionPilot.Forcing.assignmentSplice_of_lower line 129
  18. theorem OAI.PartitionPilot.Forcing.assignmentSplice_extends line 136
  19. theorem OAI.PartitionPilot.Forcing.assignmentCut_splice_below line 155
  20. theorem OAI.PartitionPilot.Forcing.assignmentUpper_splice_above line 165
  21. theorem OAI.PartitionPilot.Forcing.assignmentSplice_nested line 179