OAI/SetTheory/PartitionPrinciple/Forcing/GroundMainFinalSupportedCertificateFamilies.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.supportedEqualityCertificateBound line 13
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_supportedEqualityCertificateBound line 17
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedEqualityCertificateBound_mem line 25
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedEqualityCertificate_mem line 37
5. def OAI.PartitionPilot.Forcing.TransitiveGround.supportedEqualitySequenceEnv line 66
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_supportedEqualitySequenceEnv line 85
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.forces_supportedEqualitySequence_entry line 130
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_forced_supportedEqualitySequence line 151
9. def OAI.PartitionPilot.Forcing.TransitiveGround.supportedCertificateFamilyRelation line 192
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedCertificateFamilyRelation_mem_ordinary line 203
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedCertificateFamily_groundData line 248
12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.exists_supportedEqualityBasis line 282
13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.exists_supportedCertificateFamily line 399