OAI/SetTheory/PartitionPrinciple/Definability/NaturalStepFormulas.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.functionGraphOnFormula line 14
2. def OAI.PartitionPilot.Forcing.BoundedFormula.graphRestrictionFormula line 21
3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_graphRestrictionFormula line 25
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_functionGraphOnFormula line 48
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_graphRestrictionFormula line 63
6. def OAI.PartitionPilot.Forcing.groundRecursionStep line 80
7. def OAI.PartitionPilot.Forcing.SetFormula.ordinalRecursionTraceFormula line 86
8. def OAI.PartitionPilot.Forcing.SetFormula.ordinalSuccessorTraceFormula line 94
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_ordinalRecursionTraceFormula line 104
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_ordinalSuccessorTraceFormula line 164
11. def OAI.PartitionPilot.Forcing.SetFormula.naturalStepFormula line 198
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_naturalStepFormula line 209
13. theorem OAI.PartitionPilot.Forcing.natSetCode_succ_eq_insert_iff line 245