OAI/SetTheory/PartitionPrinciple/Definability/PreparedCertificateCodes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SynchronizedEnumerationCode line 10
2. def OAI.PartitionPilot.Forcing.BoundedFormula.synchronizedEnumerationFormula line 21
3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_synchronizedEnumerationFormula line 36
4. def OAI.PartitionPilot.Forcing.BoundedFormula.certificateEnumerationEntryFormula line 63
5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_certificateEnumerationEntryFormula line 75
6. def OAI.PartitionPilot.Forcing.PreparedCertificateCode line 109
7. def OAI.PartitionPilot.Forcing.SetFormula.preparedCertificateFormula line 120
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_preparedCertificateFormula line 135