OAI/SetTheory/PartitionPrinciple/Transfinite/GroundStageThreeAssignmentFamilies.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignment_relationLaws line 15
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentImage_eq_relationImage line 63
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignment_relationLaws line 72
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentImage_one line 76
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentImage_mul line 82
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentImage_cut line 126
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentImage_on_old line 139
  8. def OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentActionFamily line 185
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_stageTwoAssignmentActionFamily line 187
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentActionFamily_mem line 192
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentActionGraph_mem line 203
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentActionFamily_mem_of_inputs line 215
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentImage_small line 233
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentImage_eq_relationImage line 298
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignment_relationLaws line 310
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentImage_one line 314
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentImage_mul line 322
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentImage_cut line 380
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentImage_on_old line 394
  20. def OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentActionFamily line 451
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_stageThreeAssignmentActionFamily line 453
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentActionFamily_mem line 459
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentActionGraph_mem line 468
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentActionFamily_mem_of_inputs line 481
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageThreeAssignmentImage_small line 500