OAI/SetTheory/PartitionPrinciple/Definability/SupportedCertificateRelations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.supportedEqualityRelation line 12
2. theorem OAI.PartitionPilot.Forcing.pair_mem_supportedEqualityRelation line 16
3. def OAI.PartitionPilot.Forcing.BoundedFormula.supportedEqualityEntryFormula line 28
4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_supportedEqualityEntryFormula line 33
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedEqualityRelation_mem line 46
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedEqualityRelation_entry line 71
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedEqualityRelation_total line 87
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedEqualityRelation_mem_ordinary line 104
9. def OAI.PartitionPilot.Forcing.SupportedEqualityCertificate line 139
10. def OAI.PartitionPilot.Forcing.supportedCertificateRelation line 149
11. theorem OAI.PartitionPilot.Forcing.pair_mem_supportedCertificateRelation line 157
12. theorem OAI.PartitionPilot.Forcing.supportedCertificateRelation_subset line 180