OAI/SetTheory/PartitionPrinciple/Transfinite/StageTwoClosureData.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentGraph line 19
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.subset_product line 21

    Distinct definitions of this name: OAI/SetTheory/PartitionPrinciple/Transfinite/GroundStageOneSequenceProjections.lean:21 (same statement text; different proof or body). Qualify references as OAI.PartitionPilot.Forcing.TransitiveGround.subset_product@path.

  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentGraph_entry line 26
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentGraph_function line 37
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentGraph_mem line 53
  6. theorem OAI.PartitionPilot.Forcing.StageTwoCondition.completeProjection line 103
  7. def OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoSmallRestriction line 156
  8. def OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoSmallInclusion line 164
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoSmallCompleteProjection line 189
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoSmallInclusion_encode line 217
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoSmallRestriction_encode line 227
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoSmallRestriction_graph line 275
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoSmallRestriction_graph_mem line 310
  14. def OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoConditionData line 354
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoConditionData_raw line 362
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoAssignmentGraph_eq_graph line 368
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoSequence_projections_ground line 394
  18. structure OAI.PartitionPilot.Forcing.StageTwoProjectionData line 436
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoProjectionData line 493
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoCondition_lower_bound line 595
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoCondition_internally_closed line 637
  22. structure OAI.PartitionPilot.Forcing.StageTwoClosureData line 654
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoClosureData line 685