OAI/Computability/WitnessedChoice/Homogeneity.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WitnessedSeparation.Grid.occurrences_card line 16
  2. theorem OAI.WitnessedSeparation.Grid.augment_card line 23
  3. def OAI.WitnessedSeparation.Grid.namesBelow line 28
  4. theorem OAI.WitnessedSeparation.Grid.namesBelow_spare line 31
  5. theorem OAI.WitnessedSeparation.Grid.tuple_partial_shift line 39
  6. theorem OAI.WitnessedSeparation.Grid.AtomShift.stateAt_flow line 50
  7. theorem OAI.WitnessedSeparation.Grid.AtomShift.unique_on_touch line 64
  8. def OAI.WitnessedSeparation.Projection.ind line 84
  9. theorem OAI.WitnessedSeparation.Projection.ind_sq line 87
  10. theorem OAI.WitnessedSeparation.Projection.sum_ind line 90
  11. theorem OAI.WitnessedSeparation.Projection.card_sq_le_projections line 93
  12. def OAI.WitnessedSeparation.BoxLines.projection line 149
  13. def OAI.WitnessedSeparation.BoxLines.fullLines line 151
  14. def OAI.WitnessedSeparation.BoxLines.edgeBoundary line 154
  15. theorem OAI.WitnessedSeparation.BoxLines.fin_constant line 157
  16. theorem OAI.WitnessedSeparation.BoxLines.partial_line_boundary line 163
  17. theorem OAI.WitnessedSeparation.BoxLines.line_count line 182
  18. def OAI.WitnessedSeparation.Grid.edgeBoundary line 218
  19. def OAI.WitnessedSeparation.Grid.swapXY line 221
  20. def OAI.WitnessedSeparation.Grid.moveZ line 223
  21. theorem OAI.WitnessedSeparation.Grid.swapXY_injective line 225
  22. theorem OAI.WitnessedSeparation.Grid.moveZ_injective line 230
  23. theorem OAI.WitnessedSeparation.Grid.boundary_x_le line 235
  24. theorem OAI.WitnessedSeparation.Grid.boundary_y_le line 245
  25. theorem OAI.WitnessedSeparation.Grid.boundary_z_le line 268
  26. theorem OAI.WitnessedSeparation.Grid.projection_line_bounds line 291
  27. def OAI.WitnessedSeparation.Grid.boxConstant line 316
  28. theorem OAI.WitnessedSeparation.Grid.boxConstant_pos line 318
  29. theorem OAI.WitnessedSeparation.Grid.boundary_algebra line 324
  30. theorem OAI.WitnessedSeparation.Grid.box_boundary line 356
  31. abbrev OAI.WitnessedSeparation.Flows.Scalar line 395
  32. def OAI.WitnessedSeparation.Flows.incidence line 399
  33. theorem OAI.WitnessedSeparation.Flows.incidence_single line 405
  34. def OAI.WitnessedSeparation.Flows.edgeRelation line 414
  35. def OAI.WitnessedSeparation.Flows.connected line 417
  36. abbrev OAI.WitnessedSeparation.Flows.Component line 420
  37. def OAI.WitnessedSeparation.Flows.component line 422
  38. theorem OAI.WitnessedSeparation.Flows.mem_component line 428
  39. theorem OAI.WitnessedSeparation.Flows.edge_connected line 432
  40. theorem OAI.WitnessedSeparation.Flows.path_flow line 437
  41. theorem OAI.WitnessedSeparation.Flows.sum_single line 458
  42. theorem OAI.WitnessedSeparation.Flows.sum_incidence line 463
  43. theorem OAI.WitnessedSeparation.Flows.sum_incidence_component line 473
  44. theorem OAI.WitnessedSeparation.Flows.solvable_iff line 490
  45. theorem OAI.WitnessedSeparation.Flows.partial_flow_iff line 537
  46. instance OAI.WitnessedSeparation.Flows.(instance at line 568) line 568
  47. def OAI.WitnessedSeparation.Flows.cell line 570
  48. def OAI.WitnessedSeparation.Flows.quotientMap line 572
  49. theorem OAI.WitnessedSeparation.Flows.mem_cell line 575
  50. theorem OAI.WitnessedSeparation.Flows.cell_nonempty line 585
  51. theorem OAI.WitnessedSeparation.Flows.cells_disjoint line 589
  52. theorem OAI.WitnessedSeparation.Flows.sum_cells line 596
  53. theorem OAI.WitnessedSeparation.Flows.sum_card_cells line 608
  54. def OAI.WitnessedSeparation.Flows.edgeBoundary line 611
  55. theorem OAI.WitnessedSeparation.Flows.boundary_cell_subset line 613
  56. theorem OAI.WitnessedSeparation.Flows.sum_boundary_cells line 622
  57. theorem OAI.WitnessedSeparation.Flows.small_failing_component line 653
  58. theorem OAI.WitnessedSeparation.Grid.bound_of_boundary line 691
  59. theorem OAI.WitnessedSeparation.Grid.small_cell_bound line 701
  60. theorem OAI.WitnessedSeparation.Grid.partial_flow_small_obstruction line 708
  61. theorem OAI.WitnessedSeparation.Grid.sum_rpow_le line 737
  62. theorem OAI.WitnessedSeparation.Grid.small_components_bound line 752
  63. theorem OAI.WitnessedSeparation.Grid.exists_giant line 773
  64. theorem OAI.WitnessedSeparation.Flows.connected_mono line 801
  65. theorem OAI.WitnessedSeparation.Flows.component_mono line 812
  66. theorem OAI.WitnessedSeparation.Flows.component_eq line 818
  67. def OAI.WitnessedSeparation.Flows.IsGiant line 824
  68. theorem OAI.WitnessedSeparation.Flows.giant_mono line 828
  69. theorem OAI.WitnessedSeparation.Flows.giants_connected line 832
  70. theorem OAI.WitnessedSeparation.Flows.component_isolated line 848
  71. theorem OAI.WitnessedSeparation.Flows.giant_ne_isolated line 863
  72. theorem OAI.WitnessedSeparation.Grid.grid_connected line 885
  73. theorem OAI.WitnessedSeparation.Grid.grid_empty_component line 906
  74. theorem OAI.WitnessedSeparation.Grid.grid_empty_giant line 909
  75. theorem OAI.WitnessedSeparation.Grid.AtomShift.config_boundary line 927
  76. theorem OAI.WitnessedSeparation.Grid.quantitative_homogeneity_shift line 933
  77. theorem OAI.WitnessedSeparation.Grid.central_atomShift line 997
  78. theorem OAI.WitnessedSeparation.Grid.quantitative_homogeneity line 1024
  79. theorem OAI.WitnessedSeparation.Grid.empty_homogeneity line 1034
  80. theorem OAI.WitnessedSeparation.Counting.Formula.eval_of_partialBijectionSystem line 1051