OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixLimitBottom.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitLE line 18
  2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.point_order_congr line 24
  3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitLE_bounds line 47
  4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitLE_at line 52
  5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitLE_refl line 63
  6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitLE_antisymm line 67
  7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitLE_trans line 75
  8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointLabels_rank_lt line 96
  9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointRelation_rank_lt line 100
  10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoints_rank_lt line 104
  11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_rank_lt line 107
  12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointInclusions_rank_lt line 111
  13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorLabels_rank_lt line 116
  14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorRelation_rank_lt line 120
  15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActors_rank_lt line 124
  16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorMap_rank_lt line 127
  17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitActorInclusions_rank_lt line 131
  18. def OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitMeet line 148
  19. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeet_bounds line 155
  20. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeet_lower_left line 161
  21. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeet_lower_right line 166
  22. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeet_greatest line 171
  23. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeet_total line 201
  24. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeet_unique line 210
  25. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeet_at line 216
  26. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMultiplication line 238
  27. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInverse line 241
  28. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMultiplication_ground line 244
  29. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInverse_ground line 248
  30. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMultiplication_entry line 252
  31. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInverse_entry line 277
  32. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMultiplication_function line 299
  33. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInverse_function line 309
  34. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMultiplication_at line 317
  35. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInverse_at line 325
  36. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMultiplication_rank_lt line 331
  37. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitInverse_rank_lt line 335
  38. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_limitTransitionRow line 351
  39. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitOrder line 419
  40. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeetGraph line 423
  41. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitOrder_ground line 427
  42. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeetGraph_ground line 432
  43. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitOrder_entry line 437
  44. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeetGraph_entry line 459
  45. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitOrder_code line 484
  46. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeet_code line 492
  47. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_order_iff line 510
  48. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_meetEmbedding line 518
  49. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitOrder_rank_lt line 530
  50. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMeetGraph_rank_lt line 534
  51. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBottom line 538
  52. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBottom_mem line 541
  53. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBottom_ground line 544
  54. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBottom_eq line 547
  55. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBottom_least line 552
  56. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_bottom line 559
  57. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBottom_rank_lt line 564