OAI/SetTheory/PartitionPrinciple/Geometry/GroundCertificateProfileImageFamilies.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.TransitiveGround.synchronizedEnumerationBound line 14
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.synchronizedEnumerationBound_mem line 17
  3. def OAI.PartitionPilot.Forcing.TransitiveGround.certificateEnumerationRelation line 27
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_certificateEnumerationRelation line 35
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateEnumerationRelation_mem line 51
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_supportedCertificateEnumerations line 80
  7. def OAI.PartitionPilot.Forcing.PreparedCertificateFamilyCode line 141
  8. def OAI.PartitionPilot.Forcing.SetFormula.preparedFamilyEntries line 150
  9. def OAI.PartitionPilot.Forcing.SetFormula.preparedCertificateFamilyFormula line 164
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_preparedCertificateFamilyFormula line 174
  11. def OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileGraph line 251
  12. def OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileImage line 256
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileGraph_function line 259
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_certificateProfileGraph line 267
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_certificateProfileImage line 285
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileGraph_mem line 300
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileImage_mem_small line 315
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileImage_meetFilter line 332
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileImage_eq_of_domain_subset line 346
  20. def OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileImageFamily line 361
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_certificateProfileImageFamily line 366
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_certificateProfileImageFamily line 377
  23. def OAI.PartitionPilot.Forcing.TransitiveGround.profileRelationImageDefinition line 389
  24. def OAI.PartitionPilot.Forcing.TransitiveGround.profileImageDefinition line 401
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileImageFamily_mem line 414
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateProfileImageFamily_function line 439