OAI/SetTheory/PartitionPrinciple/Geometry/NodeCoding.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.Union line 15
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.birth line 17
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.inclusion line 21
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.inclusion_step line 26
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.inclusion_birth line 29
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.inclusion_injective line 37
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.inclusion_original line 63
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.raise_exists line 70
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_cover line 79
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.pair_cover line 84
  11. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.UnionLe line 92
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_le_stage line 95
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_le_refl line 109
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_le_trans line 113
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_le_antisymm line 126
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_le_meet_stage line 131
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_meet_exists line 150
  18. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionMeet line 159
  19. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionOrder line 161
  20. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.inclusionEmbedding line 171
  21. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.originalEmbedding line 182
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_top line 185
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_bottom line 190
  24. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionCompression line 202
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionCompression_inclusion line 206
  26. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionAction line 219
  27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionAction_inclusion line 223
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionAction_one line 235
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionAction_mul line 239
  30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionAction_left line 244
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionAction_right line 248
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionAction_order line 252
  33. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionAutomorphism line 259
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionCompression_order line 263
  35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionCompression_meet line 270
  36. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionCompressionEmbedding line 286
  37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_equivariant line 291
  38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_agreement line 299
  39. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionCap line 309
  40. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionCap_stage line 311
  41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_range_below_cap line 317
  42. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_base_agreement line 323
  43. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_action_source line 333
  44. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_maps_base line 338
  45. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.UnionOriginal line 348
  46. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_cap_separation line 350
  47. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_original_below_cap line 374
  48. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_cap_strict line 379
  49. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_separator_not_below_cap line 389
  50. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_original_shadow line 393
  51. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_accounting line 399
  52. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_base_filled line 421
  53. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_surjective_ideal line 430
  54. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionCompressionIso line 436
  55. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.unionCompressionIso_value line 441
  56. def OAI.PartitionPilot.Compression.RecursiveMaps.imageFamily line 452
  57. theorem OAI.PartitionPilot.Compression.RecursiveMaps.positive_imageFamily line 456
  58. theorem OAI.PartitionPilot.Compression.RecursiveMaps.positiveOver_imageFamily line 465
  59. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.StageProfile line 481
  60. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.first_stage_profile line 487
  61. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stage_profile line 505
  62. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_positive_stage line 538
  63. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_profile_at_stage line 550
  64. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_profile line 575
  65. structure OAI.PartitionPilot.Compression.RecursiveMaps.CompressionAlgebra line 590
  66. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.compressionAlgebra line 629
  67. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_equal_base_caps line 649
  68. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.componentWord line 671
  69. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.componentWord_length line 675
  70. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.componentWord_injective line 683
  71. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.templateOriginal line 696
  72. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.nodeCode line 701
  73. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.nodeCode_injective line 705
  74. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_coding_bound line 739
  75. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.union_size_transfer line 743