OAI/SetTheory/PartitionPrinciple/Definability/MainLimitCoverageFormulas.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.orderAntichainFormula line 12
  2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_orderAntichainFormula line 18
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.relativeMaximalAntichainFormula line 28
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_relativeMaximalAntichainFormula line 34
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.exGraphFields line 46
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_exGraphFields line 50
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.exLinkedCoverageFields line 70
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_exLinkedCoverageFields line 77
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.exMainLimitStageFields line 114
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_exMainLimitStageFields line 120
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.exMainLimitConeFields line 144
  12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_exMainLimitConeFields line 150
  13. def OAI.PartitionPilot.Forcing.BoundedFormula.certificateGraphEntryAt line 181
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_certificateGraphEntryAt line 186
  15. def OAI.PartitionPilot.Forcing.BoundedFormula.enumerationGraphEntryAt line 201
  16. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_enumerationGraphEntryAt line 205
  17. def OAI.PartitionPilot.Forcing.BoundedFormula.relativeAntichainFamilyFormula line 222
  18. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_relativeAntichainFamilyFormula line 226
  19. def OAI.PartitionPilot.Forcing.BoundedFormula.assignmentQueryWithinFormula line 245
  20. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_assignmentQueryWithinFormula line 248
  21. def OAI.PartitionPilot.Forcing.BoundedFormula.representativeIndexAdditionsMemberFormula line 256
  22. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_representativeIndexAdditionsMemberFormula line 266
  23. def OAI.PartitionPilot.Forcing.BoundedFormula.supportedCertificateFormula line 290
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_supportedCertificateFormula line 306
  25. def OAI.PartitionPilot.Forcing.BoundedFormula.supportedCertificateEntryFormula line 318
  26. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_supportedCertificateEntryFormula line 337
  27. def OAI.PartitionPilot.Forcing.BoundedFormula.exMainLimitImageFields line 368
  28. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_exMainLimitImageFields line 374
  29. def OAI.PartitionPilot.Forcing.BoundedFormula.mainLimitImageFormula line 403
  30. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainLimitImageFormula line 406
  31. def OAI.PartitionPilot.Forcing.BoundedFormula.mainLimitOldCutoffFormula line 417
  32. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainLimitOldCutoffFormula line 421
  33. def OAI.PartitionPilot.Forcing.BoundedFormula.mainLimitPointCoverageFormula line 436
  34. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainLimitPointCoverageFormula line 442
  35. def OAI.PartitionPilot.Forcing.BoundedFormula.mainLimitActorCoverageFormula line 456
  36. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainLimitActorCoverageFormula line 460
  37. def OAI.PartitionPilot.Forcing.BoundedFormula.mainLimitStrictTopFormula line 470
  38. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainLimitStrictTopFormula line 477
  39. def OAI.PartitionPilot.Forcing.BoundedFormula.mainLimitCutoffFormula line 487
  40. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainLimitCutoffFormula line 493
  41. def OAI.PartitionPilot.Forcing.BoundedFormula.mainLimitTopBirthFormula line 514
  42. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainLimitTopBirthFormula line 519
  43. def OAI.PartitionPilot.Forcing.BoundedFormula.mainLimitCoverageFormula line 533
  44. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainLimitCoverageFormula line 539
  45. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_mainLimitCoverageFormula line 549