OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixLimitCoverageConstruction.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitIdentity_ground line 21
  2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitIdentity_rank_lt line 24
  3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitGroup_code line 28
  4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorMap_multiplication_iff line 73
  5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorMap_groupEmbedding line 84
  6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorMap_inverse_iff line 94
  7. structure OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage line 102
  8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_fixedTopMainStage line 121
  9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.carrier_rank_lt line 207
  10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.actors_rank_lt line 212
  11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.carrier_below line 217
  12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.actors_below line 227
  13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.height_rank_lt line 233
  14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.code_rank_lt line 241
  15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.invariant_inputs line 249
  16. def OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.transition line 277
  17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.transition_points line 318
  18. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.transition_actors line 320
  19. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.point_strict_top line 322
  20. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronology_source_entries line 342
  21. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronology_raw_witnesses line 354
  22. theorem OAI.PartitionPilot.Forcing.relationCompose_enlargeCodomain line 405
  23. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.transition_comp line 431
  24. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_limitSerialization line 457
  25. def OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.chronologyValues line 495
  26. structure OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology line 501
  27. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.exists_rankedChronology line 512
  28. def OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.main line 573
  29. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.main_stage line 584
  30. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.main_cutoff line 586
  31. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.main_birth line 588
  32. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.agreement line 591
  33. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.history_values line 595
  34. def OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.transition line 617
  35. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.transition_map line 632
  36. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.transition_points line 634
  37. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.transition_actors line 636
  38. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.coversOldBirths line 638
  39. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.invariant line 662
  40. def OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.linked line 672
  41. def OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.cone line 680
  42. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.cone_coverage line 689
  43. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_rankedAppendLimit line 696
  44. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_coverage_iff line 769
  45. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorMap_coverage_iff line 779
  46. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.limitCoverage line 793