OAI/SetTheory/PartitionPrinciple/Geometry/Compression.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.MeetOrder line 12
  2. theorem OAI.PartitionPilot.meet_comm line 22
  3. structure OAI.PartitionPilot.MeetEmbedding line 28
  4. def OAI.PartitionPilot.Positive line 34
  5. def OAI.PartitionPilot.Profile line 37
  6. def OAI.PartitionPilot.PositiveOver line 42
  7. def OAI.PartitionPilot.ProfileOver line 47
  8. def OAI.PartitionPilot.HasOldShadow line 54
  9. def OAI.PartitionPilot.IsGreatest line 62
  10. def OAI.PartitionPilot.PermittedExtension line 65
  11. theorem OAI.PartitionPilot.profile_at_shadow line 70
  12. theorem OAI.PartitionPilot.profile_persists_one_step line 107
  13. def OAI.PartitionPilot.NodeProfile line 152
  14. def OAI.PartitionPilot.ProfileOn line 157
  15. def OAI.PartitionPilot.ShadowIn line 161
  16. def OAI.PartitionPilot.GreatestIn line 167
  17. def OAI.PartitionPilot.ContainsAnchors line 170
  18. theorem OAI.PartitionPilot.profile_on_shadow line 173
  19. def OAI.PartitionPilot.SuccessorNodes line 206
  20. def OAI.PartitionPilot.StageCases line 210
  21. theorem OAI.PartitionPilot.profile_at_every_stage line 217
  22. theorem OAI.PartitionPilot.profile_persists_through_growth line 261
  23. structure OAI.PartitionPilot.Attachment.Data line 286
  24. def OAI.PartitionPilot.Attachment.FreshLe line 305
  25. def OAI.PartitionPilot.Attachment.Le line 308
  26. theorem OAI.PartitionPilot.Attachment.not_upper_shadow line 314
  27. theorem OAI.PartitionPilot.Attachment.fresh_shadow_mono line 319
  28. theorem OAI.PartitionPilot.Attachment.fresh_trans line 325
  29. theorem OAI.PartitionPilot.Attachment.fresh_antisymm line 335
  30. theorem OAI.PartitionPilot.Attachment.le_refl line 346
  31. theorem OAI.PartitionPilot.Attachment.le_trans line 351
  32. theorem OAI.PartitionPilot.Attachment.le_antisymm line 381
  33. theorem OAI.PartitionPilot.Attachment.fresh_same_component line 393
  34. theorem OAI.PartitionPilot.Attachment.fresh_different_components line 403
  35. def OAI.PartitionPilot.Attachment.IsMeet line 413
  36. theorem OAI.PartitionPilot.Attachment.old_meet line 416
  37. theorem OAI.PartitionPilot.Attachment.shadow_meet line 424
  38. theorem OAI.PartitionPilot.Attachment.cross_meet line 436
  39. def OAI.PartitionPilot.Attachment.ComponentMeets line 456
  40. theorem OAI.PartitionPilot.Attachment.inside_mediated_impossible line 463
  41. theorem OAI.PartitionPilot.Attachment.component_fresh_meet line 468
  42. theorem OAI.PartitionPilot.Attachment.component_old_meet line 495
  43. theorem OAI.PartitionPilot.Attachment.meet_of_le line 514
  44. theorem OAI.PartitionPilot.Attachment.meet_symm line 517
  45. theorem OAI.PartitionPilot.Attachment.all_meets line 521
  46. def OAI.PartitionPilot.Attachment.meetOrder line 551
  47. theorem OAI.PartitionPilot.Attachment.meet_eq line 562
  48. def OAI.PartitionPilot.Attachment.oldEmbedding line 570
  49. theorem OAI.PartitionPilot.Attachment.has_old_shadow line 576
  50. theorem OAI.PartitionPilot.Attachment.permitted_extension line 582
  51. theorem OAI.PartitionPilot.Attachment.attachment_preserves_profile line 589
  52. def OAI.PartitionPilot.Attachment.idealOrder line 604
  53. def OAI.PartitionPilot.Attachment.cut line 615
  54. theorem OAI.PartitionPilot.Attachment.cut_mono line 618
  55. theorem OAI.PartitionPilot.Attachment.cut_meet line 622
  56. theorem OAI.PartitionPilot.Attachment.cut_of_le line 635
  57. structure OAI.PartitionPilot.Attachment.Templates line 640
  58. def OAI.PartitionPilot.Attachment.Templates.Fresh line 660
  59. def OAI.PartitionPilot.Attachment.Templates.base line 662
  60. def OAI.PartitionPilot.Attachment.Templates.shadow line 664
  61. def OAI.PartitionPilot.Attachment.Templates.Inside line 666
  62. theorem OAI.PartitionPilot.Attachment.Templates.inside_refl line 669
  63. theorem OAI.PartitionPilot.Attachment.Templates.inside_trans line 671
  64. theorem OAI.PartitionPilot.Attachment.Templates.inside_antisymm line 682
  65. theorem OAI.PartitionPilot.Attachment.Templates.inside_shadow line 692
  66. def OAI.PartitionPilot.Attachment.Templates.data line 700
  67. theorem OAI.PartitionPilot.Attachment.Templates.mapped_cut_meet line 717
  68. theorem OAI.PartitionPilot.Attachment.Templates.component_meets line 724
  69. def OAI.PartitionPilot.Attachment.Templates.extension line 752
  70. def OAI.PartitionPilot.Attachment.Templates.oldEmbedding line 754
  71. theorem OAI.PartitionPilot.Attachment.Templates.shadow_verified line 757
  72. theorem OAI.PartitionPilot.Attachment.Templates.persistence line 760
  73. def OAI.PartitionPilot.Attachment.Templates.represent line 765
  74. theorem OAI.PartitionPilot.Attachment.Templates.represent_old line 771
  75. theorem OAI.PartitionPilot.Attachment.Templates.represent_new line 775
  76. theorem OAI.PartitionPilot.Attachment.Templates.represent_le_iff line 779
  77. theorem OAI.PartitionPilot.Attachment.Templates.old_below_represent line 816
  78. theorem OAI.PartitionPilot.Attachment.Templates.upper_shadow_below_represent line 826
  79. theorem OAI.PartitionPilot.Attachment.Templates.foreign_below_represent line 837
  80. theorem OAI.PartitionPilot.Attachment.Templates.represented_meet line 849
  81. def OAI.PartitionPilot.Attachment.Templates.templateEmbedding line 876
  82. theorem OAI.PartitionPilot.Attachment.Templates.template_agrees_on_base line 881
  83. theorem OAI.PartitionPilot.Attachment.Templates.greatest_preserved line 886
  84. theorem OAI.PartitionPilot.Attachment.Templates.least_preserved line 895
  85. theorem OAI.PartitionPilot.Attachment.Templates.cross_meet_eq line 902
  86. theorem OAI.PartitionPilot.Attachment.Templates.old_lower_iff line 908
  87. theorem OAI.PartitionPilot.Attachment.Templates.old_upper_iff line 911
  88. theorem OAI.PartitionPilot.Attachment.Templates.cross_le_iff line 914
  89. theorem OAI.PartitionPilot.Attachment.Templates.shadow_meet_eq line 918
  90. theorem OAI.PartitionPilot.Attachment.Templates.template_preserves_zero line 923
  91. theorem OAI.PartitionPilot.meet_eq_left_of_le line 937
  92. def OAI.PartitionPilot.Attachment.Templates.originalFamily line 945
  93. theorem OAI.PartitionPilot.Attachment.Templates.positive_old_iff line 949
  94. theorem OAI.PartitionPilot.Attachment.Templates.positive_new_iff line 959
  95. def OAI.PartitionPilot.Attachment.Templates.cap line 969
  96. theorem OAI.PartitionPilot.Attachment.Templates.cap_shadow line 972
  97. theorem OAI.PartitionPilot.Attachment.Templates.cap_strict_above_base line 984
  98. theorem OAI.PartitionPilot.Attachment.Templates.separator_not_below_cap line 995
  99. theorem OAI.PartitionPilot.Attachment.Templates.initial_profile line 1004
  100. theorem OAI.PartitionPilot.Attachment.Templates.cap_alternatives line 1049
  101. theorem OAI.PartitionPilot.Attachment.Templates.equal_base_caps_meet line 1075
  102. theorem OAI.PartitionPilot.Attachment.Templates.initial_profile_persists line 1099
  103. structure OAI.PartitionPilot.Compression.MeetFilter line 1115
  104. def OAI.PartitionPilot.Compression.pushFilter line 1121
  105. theorem OAI.PartitionPilot.Compression.pushFilter_trace line 1137
  106. theorem OAI.PartitionPilot.Compression.pushFilter_lower_bound line 1146
  107. structure OAI.PartitionPilot.Compression.MeetIso line 1153
  108. theorem OAI.PartitionPilot.Compression.filter_image_from_slice line 1159
  109. theorem OAI.PartitionPilot.Compression.filter_images_agree line 1174
  110. theorem OAI.PartitionPilot.Compression.meet_insert_upper line 1186
  111. theorem OAI.PartitionPilot.Compression.base_meet_patch line 1194
  112. theorem OAI.PartitionPilot.Compression.base_ideal_filled line 1212
  113. theorem OAI.PartitionPilot.Compression.range_completion_from_accounting line 1223
  114. theorem OAI.PartitionPilot.Compression.embedding_injective line 1251
  115. def OAI.PartitionPilot.Compression.isoOntoIdeal line 1261
  116. structure OAI.PartitionPilot.Compression.InitialTasks line 1273
  117. def OAI.PartitionPilot.Compression.InitialTasks.batch line 1286
  118. def OAI.PartitionPilot.Compression.InitialTasks.copy line 1303
  119. theorem OAI.PartitionPilot.Compression.InitialTasks.copy_agrees_on_base line 1306
  120. theorem OAI.PartitionPilot.Compression.InitialTasks.copy_initial_profile line 1310
  121. theorem OAI.PartitionPilot.Compression.InitialTasks.copy_cap_separation line 1319