OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixConePreservation.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.PartitionPilot.Forcing.GroundMainPrefix.withTopSmall line 18
  2. def OAI.PartitionPilot.Forcing.GroundMainPrefix.appendKey line 22
  3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendKey_injective line 26
  4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendKey_order line 43
  5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendKey_range line 61
  6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.indices_of_greatest line 75
  7. def OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLinked line 88
  8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendStageGraph_eq line 93
  9. theorem OAI.PartitionPilot.Forcing.relationCompose_uniformSource_eq line 115
  10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_appendRow line 138
  11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.restrictedKey_range line 208
  12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.restrictedStageGraph_eq line 220
  13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.restrictedTransitionGraph_eq line 228
  14. def OAI.PartitionPilot.Forcing.GroundMainPrefix.restrict line 252
  15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.restrict_indices line 269
  16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.restrict_stageGraph line 272
  17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.restrict_transitionGraph line 276
  18. def OAI.PartitionPilot.Forcing.GroundMainPrefix.appendTransitionGraph line 293
  19. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendTransitionGraph_eq line 297
  20. def OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone line 331
  21. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.restrict_code_rank_lt line 371
  22. def OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast line 405
  23. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_indices line 413
  24. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_linked_old line 417
  25. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_linked_top line 420
  26. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_transition_old line 423
  27. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_transition_to_top line 427
  28. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_transition_last line 432
  29. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_stageGraph line 438
  30. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_row line 443
  31. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_stageGraph_restrict line 456
  32. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_transitionGraph_restrict line 463
  33. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.field_rank_le_linkedCode line 494
  34. def OAI.PartitionPilot.Forcing.GroundMainPrefix.appendSourceBound line 512
  35. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendSourceBound_rank_le line 517
  36. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendRow_subset line 527
  37. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendRow_rank_lt line 564
  38. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_code_rank_lt line 586
  39. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_indices line 632
  40. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_stage_old line 636
  41. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_stage_top line 640
  42. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_linked_old line 643
  43. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_linked_top line 646
  44. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_transition_old line 649
  45. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_transition_to_top line 653
  46. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_transition_top line 657
  47. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_stageGraph line 662
  48. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_transitionGraph line 667
  49. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_stageGraph_restrict line 674
  50. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_transitionGraph_restrict line 681
  51. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_code_rank_lt line 703