OAI/SetTheory/PartitionPrinciple/Forcing/GroundStructuralForcingHistoryConstruction.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.small_refinementConditionFamily_prefix line 16
  2. def OAI.PartitionPilot.Forcing.rawFlatForcingStage line 73
  3. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_emptyFromGround line 81
  4. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_rawFlatForcingStage line 90
  5. def OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingStageFromCarrier line 117
  6. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_structuralForcingStageFromCarrier line 123
  7. def OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingStage line 143
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingStage_mem line 155
  9. def OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingStageFormula line 167
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_structuralForcingStageFormula line 176
  11. def OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingStepFormula line 246
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_structuralForcingStepFormula line 250
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingStepClosure line 260
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_structuralForcingTrace line 282
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralTrace_prefix_ground line 326
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralTrace_stageWitnesses line 343
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingStage_eq line 381
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingTrace_recursiveOrder line 397
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingTrace_stageOrderTop line 410
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingTrace_small_family_prefix line 442
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_structuralForcingHistory line 477