OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixLimitGroupLaws.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.directLimitRelation line 11
  2. theorem OAI.PartitionPilot.Forcing.directLimitRelation_subset line 18
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_directLimitRelation line 21
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.directLimitRelationEntryFormula line 45
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_directLimitRelationEntryFormula line 52
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.directLimitRelation_mem line 72
  7. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.relation_iff line 99
  8. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.relation_equivalence line 118
  9. def OAI.PartitionPilot.Forcing.directLimitCarrier line 143
  10. def OAI.PartitionPilot.Forcing.directLimitInclusion line 147
  11. def OAI.PartitionPilot.Forcing.CodedDirectPresentation.limitPoint line 155
  12. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.limitPoint_mem line 159
  13. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.limitPoint_eq_iff_related line 163
  14. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.limitPoint_same_iff line 169
  15. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.limitPoint_transition line 174
  16. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.limitPoint_later_iff line 180
  17. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.inclusion_entry line 185
  18. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.inclusion_injection line 190
  19. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.inclusion_comp line 199
  20. theorem OAI.PartitionPilot.Forcing.indexedCarrierLabels_rank_lt line 227
  21. theorem OAI.PartitionPilot.Forcing.directLimitRelation_rank_lt line 234
  22. theorem OAI.PartitionPilot.Forcing.equivalenceClasses_rank_lt line 240
  23. theorem OAI.PartitionPilot.Forcing.equivalenceClassifier_rank_lt line 248
  24. theorem OAI.PartitionPilot.Forcing.indexedClassInclusion_rank_lt line 256
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedClassInclusions_rank_lt line 267
  26. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.limitPoint_coverage line 290
  27. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.mixed_pair_coverage line 296
  28. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.mixed_triple_coverage line 309
  29. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.pair_coverage line 327
  30. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.triple_coverage line 333
  31. def OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap line 348
  32. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_subset line 353
  33. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_entry line 356
  34. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_at line 368
  35. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_function line 378
  36. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_injection line 388
  37. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_triangle line 395
  38. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_range line 411
  39. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_onto line 421
  40. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_unique line 425
  41. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_eq_indexedValueLift line 457
  42. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_ground line 483
  43. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_injection_into line 508
  44. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.coneMap_bijection_onto line 517
  45. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointLabels line 535
  46. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointRelation line 538
  47. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoints line 541
  48. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap line 544
  49. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointInclusions line 547
  50. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointLabels_ground line 550
  51. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointRelation_ground line 554
  52. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoints_ground line 558
  53. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_ground line 561
  54. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointInclusions_ground line 566
  55. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_injection line 570
  56. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointInclusions_function line 574
  57. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointInclusions_entry line 578
  58. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_comp line 584
  59. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorLabels line 590
  60. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorRelation line 593
  61. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActors line 596
  62. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorMap line 599
  63. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorInclusions line 602
  64. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorLabels_ground line 605
  65. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorRelation_ground line 609
  66. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActors_ground line 613
  67. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorMap_ground line 616
  68. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorInclusions_ground line 621
  69. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorMap_injection line 625
  70. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorInclusions_function line 629
  71. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorInclusions_entry line 633
  72. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorMap_comp line 639
  73. def OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitMul line 645
  74. def OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitInv line 651
  75. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMul_bounds line 656
  76. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInv_bounds line 662
  77. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMul_total line 667
  78. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInv_total line 676
  79. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMul_unique line 684
  80. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInv_unique line 710
  81. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMul_at line 732
  82. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInv_at line 752
  83. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitIdentity line 768
  84. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitIdentity_mem line 771
  85. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitIdentity_eq line 774