OAI/SetTheory/PartitionPrinciple/Definability/GroundStandardInaccessibleFormulas.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.groundCardinalFormula line 10
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundCardinalFormula line 18
3. def OAI.PartitionPilot.Forcing.BoundedFormula.cofinalFunctionFormula line 40
4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_cofinalFunctionFormula line 46
5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_cofinalFunctionFormula line 53
6. def OAI.PartitionPilot.Forcing.SetFormula.groundCofinalRegularFormula line 63
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundCofinalRegularFormula line 72
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundCofinalRegularFormula_iff_regular line 87
9. def OAI.PartitionPilot.Forcing.SetFormula.groundCardinalStrongLimitFormula line 98
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundCardinalStrongLimitFormula line 106
11. def OAI.PartitionPilot.Forcing.SetFormula.groundStandardInaccessibleFormula line 137
12. def OAI.PartitionPilot.Forcing.SetFormula.existsGroundStandardInaccessibleFormula line 142
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundStandardInaccessibleFormula line 150
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_existsGroundStandardInaccessibleFormula line 169
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundStandardInaccessibleFormula_iff_conditions line 180
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_existsGroundStandardInaccessibleFormula_iff_conditions line 191