OAI/SetTheory/PartitionPrinciple/Transfinite/GroundStageOneSequenceProjections.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneRowGraph line 18
  2. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentGraph line 19
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.subset_product line 21

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

  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneRowGraph_entry line 25
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentGraph_entry line 36
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneRowGraph_function line 47
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentGraph_function line 50
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneRowGraph_mem line 64
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentGraph_mem line 72
  10. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneConditionRow line 111
  11. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneConditionData line 114
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneConditionData_raw line 123
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneRowGraph_eq_graph line 128
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentGraph_eq_graph line 149
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneSequence_projections_ground line 170