OAI/SetTheory/PartitionPrinciple/Definability/RecursivePrimitiveFormulas.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.recursiveIndicesSetFormula line 12
2. def OAI.PartitionPilot.Forcing.SetFormula.pairFieldSetFormula line 16
3. def OAI.PartitionPilot.Forcing.SetFormula.indexedFreshSetFormula line 20
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_recursiveIndicesSetFormula line 33
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_pairFieldSetFormula line 55
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_pairSecondFieldSetFormula line 76
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_indexedFreshSetFormula line 85