OAI/SetTheory/PartitionPrinciple/Forcing/SymmetricGroundForcing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.nameSymmetryFormula line 9
2. def OAI.PartitionPilot.Forcing.TransitiveGround.symmetryParameters line 22
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_nameSymmetryFormula line 26
4. def OAI.PartitionPilot.Forcing.SetFormula.hereditaryStepFormula line 62
5. def OAI.PartitionPilot.Forcing.SetFormula.hereditaryCertificateFormula line 66
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_hereditaryStepFormula line 76
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.hereditaryCertificate_isName line 88
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.hereditaryCertificate_sound line 102
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_hereditary_certificate line 140
10. def OAI.PartitionPilot.Forcing.SetFormula.uniformHereditaryFormula line 189
11. def OAI.PartitionPilot.Forcing.SetFormula.liftedHereditaryFormula line 192
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_uniformHereditaryFormula line 205
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.domainMeaning_liftedHereditary line 228
14. def OAI.PartitionPilot.Forcing.SetFormula.symmetricGroundPrimitives line 264
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_symmetricGroundForcing line 276
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetricForcingSet_mem line 300