OAI/SetTheory/PartitionPrinciple/Definability/ForcingHistoryOutputFormulas.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.BoundedFormula.stageOneAssignmentsMemberFormula line 11
2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_stageOneAssignmentsMemberFormula line 15
3. def OAI.PartitionPilot.Forcing.BoundedFormula.stageOneAssignmentsSubsetFormula line 22
4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_stageOneAssignmentsSubsetFormula line 25
5. def OAI.PartitionPilot.Forcing.SetFormula.stageOneCandidateFormula line 36
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneCandidateFormula line 49
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneCandidateFormula_omega line 88
8. def OAI.PartitionPilot.Forcing.SetFormula.forcingHistoryConditionsOutputFormula line 100
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_forcingHistoryConditionsOutputFormula line 111
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_unique_forcingHistoryConditionsOutput line 134