OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixLimitCoverageGraph.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.LinkedCoverageFieldsCode line 12
  2. def OAI.PartitionPilot.Forcing.MainLimitConeEntryCode line 16
  3. def OAI.PartitionPilot.Forcing.MainLimitOldPointImageCode line 20
  4. def OAI.PartitionPilot.Forcing.MainLimitOldActorImageCode line 24
  5. def OAI.PartitionPilot.Forcing.MainLimitOldCutoffCode line 28
  6. structure OAI.PartitionPilot.Forcing.MainLimitCoverageGraphCode line 32
  7. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.coverageFields_iff line 44
  8. structure OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitCoverage line 73
  9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitCoverage.top_absent line 91
  10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitCoverage.new_point_iff line 97
  11. def OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldUnion line 113
  12. def OAI.PartitionPilot.Forcing.GroundMainPrefix.carrierUnion line 116
  13. def OAI.PartitionPilot.Forcing.GroundMainPrefix.actorUnion line 118
  14. def OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapUnion line 120
  15. def OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapUnion line 123
  16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldValues_ground line 126
  17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapValues_ground line 131
  18. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapValues_ground line 138
  19. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldUnion_ground line 145
  20. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.carrierUnion_ground line 148
  21. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorUnion_ground line 150
  22. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapUnion_ground line 152
  23. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapUnion_ground line 154
  24. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldUnion_mem line 156
  25. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapUnion_mem line 160
  26. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapUnion_mem line 164
  27. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldFamily_subset_union line 168
  28. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.carrierFamily_subset_union line 172
  29. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorFamily_subset_union line 176
  30. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapFamily_subset_union line 180
  31. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapFamily_subset_union line 184
  32. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldFamily_rank_le_code line 188
  33. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.carrierFamily_rank_le_code line 195
  34. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorFamily_rank_le_code line 198
  35. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapFamily_rank_le_code line 201
  36. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapFamily_rank_le_code line 209
  37. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldUnion_rank_le_code line 217
  38. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.carrierUnion_rank_le_code line 221
  39. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorUnion_rank_le_code line 224
  40. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapUnion_rank_le_code line 227
  41. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapUnion_rank_le_code line 230
  42. def OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffFamily line 237
  43. def OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldFamily line 240
  44. def OAI.PartitionPilot.Forcing.GroundMainPrefix.birthFamily line 243
  45. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffFamily_ground line 246
  46. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldFamily_ground line 256
  47. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialBirth_entry line 271
  48. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthFamily_ground line 278
  49. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffFamily_function line 287
  50. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldFamily_function line 290
  51. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthFamily_function line 293
  52. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffFamily_entry line 296
  53. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldFamily_entry line 300
  54. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthFamily_entry line 304
  55. def OAI.PartitionPilot.Forcing.GroundMainPrefix.pointPresentation line 312
  56. def OAI.PartitionPilot.Forcing.GroundMainPrefix.actorPresentation line 324
  57. def OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffUnion line 340
  58. def OAI.PartitionPilot.Forcing.GroundMainPrefix.birthUnion line 342
  59. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffValues_ground line 344
  60. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthValues_ground line 347
  61. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffUnion_ground line 350
  62. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthUnion_ground line 352
  63. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffUnion_mem line 354
  64. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthUnion_mem line 358
  65. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffFamily_subset_union line 362
  66. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthFamily_subset_union line 365
  67. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffFamily_rank_le_code line 368
  68. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldFamily_rank_le_code line 377
  69. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthFamily_rank_le_code line 388
  70. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffValues_rank_le_code line 393
  71. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthValues_rank_le_code line 397
  72. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffUnion_rank_le_code line 401
  73. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birthUnion_rank_le_code line 404
  74. def OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffSuccessorFamily line 421
  75. def OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffLimit line 424
  76. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffSuccessorFamily_ground line 427
  77. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffSuccessorFamily_function line 444
  78. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffSuccessorFamily_entry line 447
  79. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffSuccessorValues_ground line 452
  80. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffLimit_ground line 456
  81. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffLimit_mem line 458
  82. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoff_mem_cutoffLimit line 463
  83. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.birth_time_mem_cutoffLimit line 466
  84. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffLimit_ordinal line 470
  85. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffSuccessorFamily_rank_le_code line 476
  86. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffLimit_rank_le_code line 487
  87. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.cutoffLimit_mem_inaccessible line 490
  88. def OAI.PartitionPilot.Forcing.mainPrefixLimitTargetFields line 522
  89. def OAI.PartitionPilot.Forcing.MainPrefixLimitStepRawCode line 525
  90. def OAI.PartitionPilot.Forcing.MainPrefixLimitStepCode line 537
  91. theorem OAI.PartitionPilot.Forcing.MainPrefixLimitStepCode.extension line 547
  92. theorem OAI.PartitionPilot.Forcing.MainPrefixLimitStepCode.indices_successor line 551
  93. theorem OAI.PartitionPilot.Forcing.MainPrefixLimitStepCode.next_fields line 559
  94. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.rawFields_birth_entry line 572
  95. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitConeEntry_iff line 600
  96. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitOldPointImage_iff line 619
  97. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitOldActorImage_iff line 632
  98. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitOldCutoff_iff line 646
  99. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitCoverage_graph_iff line 662