OAI/Computability/PerfectCompleteness/Foundations/PartitionsLemmas.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CanonicalPartition.fiber line 25
  2. def OAI.PerfectCompleteness.CanonicalPartition.parts line 27
  3. abbrev OAI.PerfectCompleteness.CanonicalPartition.Part line 30
  4. def OAI.PerfectCompleteness.CanonicalPartition.label line 32
  5. instance OAI.PerfectCompleteness.CanonicalPartition.(instance at line 35) line 35
  6. instance OAI.PerfectCompleteness.CanonicalPartition.(instance at line 39) line 39
  7. def OAI.PerfectCompleteness.CanonicalPartition.representative line 43
  8. theorem OAI.PerfectCompleteness.CanonicalPartition.representative_spec line 46
  9. def OAI.PerfectCompleteness.CanonicalPartition.output line 50
  10. theorem OAI.PerfectCompleteness.CanonicalPartition.part_eq_fiber line 53
  11. theorem OAI.PerfectCompleteness.CanonicalPartition.mem_iff line 57
  12. theorem OAI.PerfectCompleteness.CanonicalPartition.part_nonempty line 62
  13. theorem OAI.PerfectCompleteness.CanonicalPartition.output_mem_range line 66
  14. theorem OAI.PerfectCompleteness.CanonicalPartition.output_label line 70
  15. theorem OAI.PerfectCompleteness.CanonicalPartition.output_injective line 75
  16. theorem OAI.PerfectCompleteness.CanonicalPartition.label_representative line 80
  17. theorem OAI.PerfectCompleteness.CanonicalPartition.label_surjective line 85
  18. theorem OAI.PerfectCompleteness.CanonicalPartition.card_parts_le line 89
  19. theorem OAI.PerfectCompleteness.CanonicalPartition.restoration_bijective line 93
  20. theorem OAI.PerfectCompleteness.CanonicalPartition.parts_eq_of_kernel_eq line 105
  21. theorem OAI.PerfectCompleteness.CanonicalPartition.kernel_le_of_parts_subset line 119
  22. theorem OAI.PerfectCompleteness.CanonicalPartition.parts_eq_iff_kernel_eq line 132
  23. theorem OAI.PerfectCompleteness.CanonicalPartition.label_val_eq_of_parts_eq line 140
  24. theorem OAI.PerfectCompleteness.CanonicalPartition.parts_postcomp_injective line 146
  25. def OAI.PerfectCompleteness.CanonicalPartition.coarsen line 152
  26. theorem OAI.PerfectCompleteness.CanonicalPartition.output_coarsen line 156
  27. theorem OAI.PerfectCompleteness.CanonicalPartition.coarsen_eq_iff line 160
  28. theorem OAI.PerfectCompleteness.CanonicalPartition.subset_coarsen line 170
  29. theorem OAI.PerfectCompleteness.CanonicalPartition.coarsen_label line 177
  30. theorem OAI.PerfectCompleteness.CanonicalPartition.coarsen_surjective line 183
  31. theorem OAI.PerfectCompleteness.CanonicalPartition.card_coarsen_fiber_le line 189
  32. theorem OAI.PerfectCompleteness.CanonicalPartition.coarsen_at_most_two line 202
  33. def OAI.PerfectCompleteness.CanonicalPartition.binaryDeletionFiberEquiv line 208
  34. theorem OAI.PerfectCompleteness.CanonicalPartition.card_binaryDeletion_fiber line 217
  35. theorem OAI.PerfectCompleteness.CanonicalPartition.binaryDeletion_at_most_two line 222
  36. theorem OAI.PerfectCompleteness.CanonicalPartition.evaluation_consistent_and_satisfying line 229
  37. def OAI.PerfectCompleteness.PointwiseSpaces.pullback line 247
  38. theorem OAI.PerfectCompleteness.PointwiseSpaces.pullback_apply line 255
  39. theorem OAI.PerfectCompleteness.PointwiseSpaces.pullback_one line 258
  40. theorem OAI.PerfectCompleteness.PointwiseSpaces.pullback_mul line 261
  41. theorem OAI.PerfectCompleteness.PointwiseSpaces.pullback_comp line 264
  42. theorem OAI.PerfectCompleteness.PointwiseSpaces.pullback_injective line 269
  43. def OAI.PerfectCompleteness.PointwiseSpaces.squareSpace line 276
  44. theorem OAI.PerfectCompleteness.PointwiseSpaces.mul_mem_squareSpace line 279
  45. theorem OAI.PerfectCompleteness.PointwiseSpaces.squareSpace_mono line 284
  46. theorem OAI.PerfectCompleteness.PointwiseSpaces.le_squareSpace line 290
  47. theorem OAI.PerfectCompleteness.PointwiseSpaces.one_mem_squareSpace line 295
  48. theorem OAI.PerfectCompleteness.PointwiseSpaces.squareSpace_pullback_le line 299
  49. theorem OAI.PerfectCompleteness.PointwiseSpaces.squareSpace_map_pullback line 308
  50. def OAI.PerfectCompleteness.PointwiseSpaces.childSpace line 322
  51. theorem OAI.PerfectCompleteness.PointwiseSpaces.child_square_le line 326
  52. theorem OAI.PerfectCompleteness.PointwiseSpaces.child_le line 331
  53. theorem OAI.PerfectCompleteness.PointwiseSpaces.one_mem_childSpace_of_child line 340
  54. theorem OAI.PerfectCompleteness.PointwiseSpaces.one_mem_childSpace line 348
  55. theorem OAI.PerfectCompleteness.PointwiseSpaces.childSpace_mono line 354
  56. theorem OAI.PerfectCompleteness.PointwiseSpaces.childSpace_pullback_le line 359
  57. def OAI.PerfectCompleteness.ProductReduction.productMap line 391
  58. theorem OAI.PerfectCompleteness.ProductReduction.productMap_apply line 394
  59. theorem OAI.PerfectCompleteness.ProductReduction.productMap_surjective line 397
  60. def OAI.PerfectCompleteness.ProductReduction.CoordinateInvariant line 405
  61. theorem OAI.PerfectCompleteness.ProductReduction.coordinateInvariant_of_update line 410
  62. theorem OAI.PerfectCompleteness.ProductReduction.CoordinateInvariant.update line 420
  63. theorem OAI.PerfectCompleteness.ProductReduction.constant_on_product_fibers line 429
  64. def OAI.PerfectCompleteness.ProductReduction.preimage line 450
  65. theorem OAI.PerfectCompleteness.ProductReduction.productMap_preimage line 454
  66. def OAI.PerfectCompleteness.ProductReduction.induced line 459
  67. theorem OAI.PerfectCompleteness.ProductReduction.induced_productMap line 464
  68. theorem OAI.PerfectCompleteness.ProductReduction.induced_factorization line 471
  69. theorem OAI.PerfectCompleteness.ProductReduction.induced_unique line 478
  70. theorem OAI.PerfectCompleteness.ProductReduction.coordinateInvariant_pullback line 489
  71. theorem OAI.PerfectCompleteness.ProductReduction.induced_eq_of_pullback line 499
  72. def OAI.PerfectCompleteness.ProjectedColumnSlice.projectedColumns line 533
  73. def OAI.PerfectCompleteness.ProjectedColumnSlice.restrictionZ line 535
  74. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.restrictionZ_val line 540
  75. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.restrictionZ_apply line 543
  76. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.restrictionZ_surjective line 546
  77. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.finrank_projectedColumns_le line 553
  78. def OAI.PerfectCompleteness.ProjectedColumnSlice.Compatible line 557
  79. def OAI.PerfectCompleteness.ProjectedColumnSlice.targetQ line 560
  80. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.targetQ_apply line 563
  81. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.targetQ_comp_restrictionZ line 566
  82. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.targetQ_independent line 572
  83. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.compatible_iff_domRestrict line 581
  84. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.target_unique line 592
  85. def OAI.PerfectCompleteness.ProjectedColumnSlice.inducedTarget line 601
  86. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.inducedTarget_comp_restrictionZ line 606
  87. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.inducedTarget_eq_targetQ line 611
  88. theorem OAI.PerfectCompleteness.ProjectedColumnSlice.compatible_iff_inducedTarget line 617
  89. def OAI.PerfectCompleteness.ProjectedColumnSlice.sliceEquiv line 624
  90. def OAI.PerfectCompleteness.PulledColumnSpace.pulled line 649
  91. theorem OAI.PerfectCompleteness.PulledColumnSpace.quotientDual_injective line 653
  92. def OAI.PerfectCompleteness.PulledColumnSpace.pulledEquiv line 657
  93. theorem OAI.PerfectCompleteness.PulledColumnSpace.pulledEquiv_val line 661
  94. theorem OAI.PerfectCompleteness.PulledColumnSpace.pulled_le_annihilator line 665
  95. theorem OAI.PerfectCompleteness.PulledColumnSpace.finrank_pulled line 675
  96. theorem OAI.PerfectCompleteness.PulledColumnSpace.finrank_pulled_le line 680
  97. def OAI.PerfectCompleteness.PulledColumnSpace.Candidates line 686
  98. instance OAI.PerfectCompleteness.PulledColumnSpace.candidatesNonempty line 690
  99. def OAI.PerfectCompleteness.PulledColumnSpace.candidateEquiv line 696
  100. theorem OAI.PerfectCompleteness.PulledColumnSpace.candidateEquiv_val line 713
  101. theorem OAI.PerfectCompleteness.PulledColumnSpace.candidate_apply_known line 718
  102. theorem OAI.PerfectCompleteness.PulledColumnSpace.card_pulled line 728
  103. theorem OAI.PerfectCompleteness.PulledColumnSpace.card_pulled_le line 734
  104. def OAI.PerfectCompleteness.PulledColumnSpace.candidatesEquivCoordinates line 740
  105. instance OAI.PerfectCompleteness.PulledColumnSpace.candidatesFintype line 747
  106. theorem OAI.PerfectCompleteness.PulledColumnSpace.card_candidates line 753
  107. theorem OAI.PerfectCompleteness.PulledColumnSpace.card_candidates_le line 758
  108. theorem OAI.PerfectCompleteness.PulledColumnSpace.fintype_card_candidates line 765