OAI/ModelTheory/Choiceless/Flows.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CPTSeparation.Projection.ind line 15
  2. theorem OAI.CPTSeparation.Projection.ind_sq line 18
  3. theorem OAI.CPTSeparation.Projection.sum_ind line 21
  4. theorem OAI.CPTSeparation.Projection.card_sq_le_projections line 24
  5. def OAI.CPTSeparation.BoxLines.projection line 78
  6. def OAI.CPTSeparation.BoxLines.fullLines line 80
  7. def OAI.CPTSeparation.BoxLines.edgeBoundary line 83
  8. theorem OAI.CPTSeparation.BoxLines.fin_constant line 86
  9. theorem OAI.CPTSeparation.BoxLines.partial_line_boundary line 92
  10. theorem OAI.CPTSeparation.BoxLines.line_count line 111
  11. def OAI.CPTSeparation.Grid.edgeBoundary line 147
  12. def OAI.CPTSeparation.Grid.swapXY line 150
  13. def OAI.CPTSeparation.Grid.moveZ line 152
  14. theorem OAI.CPTSeparation.Grid.swapXY_injective line 154
  15. theorem OAI.CPTSeparation.Grid.moveZ_injective line 159
  16. theorem OAI.CPTSeparation.Grid.boundary_x_le line 164
  17. theorem OAI.CPTSeparation.Grid.boundary_y_le line 174
  18. theorem OAI.CPTSeparation.Grid.boundary_z_le line 197
  19. theorem OAI.CPTSeparation.Grid.projection_line_bounds line 220
  20. def OAI.CPTSeparation.Grid.boxConstant line 241
  21. theorem OAI.CPTSeparation.Grid.boxConstant_pos line 243
  22. theorem OAI.CPTSeparation.Grid.boundary_algebra line 249
  23. theorem OAI.CPTSeparation.Grid.box_boundary line 281
  24. abbrev OAI.CPTSeparation.Flows.Scalar line 318
  25. def OAI.CPTSeparation.Flows.incidence line 322
  26. theorem OAI.CPTSeparation.Flows.incidence_single line 328
  27. def OAI.CPTSeparation.Flows.edgeRelation line 343
  28. def OAI.CPTSeparation.Flows.connected line 346
  29. abbrev OAI.CPTSeparation.Flows.Component line 349
  30. def OAI.CPTSeparation.Flows.component line 351
  31. theorem OAI.CPTSeparation.Flows.mem_component line 357
  32. theorem OAI.CPTSeparation.Flows.edge_connected line 370
  33. theorem OAI.CPTSeparation.Flows.path_flow line 384
  34. theorem OAI.CPTSeparation.Flows.sum_single line 414
  35. theorem OAI.CPTSeparation.Flows.sum_incidence line 422
  36. theorem OAI.CPTSeparation.Flows.sum_incidence_component line 440
  37. theorem OAI.CPTSeparation.Flows.solvable_iff line 457
  38. theorem OAI.CPTSeparation.Flows.partial_flow_iff line 504
  39. instance OAI.CPTSeparation.Flows.(instance at line 529) line 529
  40. def OAI.CPTSeparation.Flows.cell line 531
  41. def OAI.CPTSeparation.Flows.quotientMap line 533
  42. theorem OAI.CPTSeparation.Flows.mem_cell line 536
  43. theorem OAI.CPTSeparation.Flows.cell_nonempty line 555
  44. theorem OAI.CPTSeparation.Flows.cells_disjoint line 568
  45. theorem OAI.CPTSeparation.Flows.sum_cells line 584
  46. theorem OAI.CPTSeparation.Flows.sum_card_cells line 605
  47. def OAI.CPTSeparation.Flows.edgeBoundary line 617
  48. theorem OAI.CPTSeparation.Flows.boundary_cell_subset line 619
  49. theorem OAI.CPTSeparation.Flows.sum_boundary_cells line 628
  50. theorem OAI.CPTSeparation.Flows.small_failing_component line 657
  51. theorem OAI.CPTSeparation.Grid.bound_of_boundary line 698
  52. theorem OAI.CPTSeparation.Grid.small_cell_bound line 708
  53. theorem OAI.CPTSeparation.Grid.partial_flow_small_obstruction line 715
  54. theorem OAI.CPTSeparation.Grid.sum_rpow_le line 744
  55. theorem OAI.CPTSeparation.Grid.small_components_bound line 759
  56. theorem OAI.CPTSeparation.Grid.exists_giant line 780
  57. theorem OAI.CPTSeparation.Flows.connected_mono line 802
  58. theorem OAI.CPTSeparation.Flows.component_mono line 821
  59. theorem OAI.CPTSeparation.Flows.component_eq line 835
  60. def OAI.CPTSeparation.Flows.IsGiant line 849
  61. theorem OAI.CPTSeparation.Flows.giant_mono line 853
  62. theorem OAI.CPTSeparation.Flows.giants_connected line 865
  63. theorem OAI.CPTSeparation.Flows.component_isolated line 888
  64. theorem OAI.CPTSeparation.Flows.giant_ne_isolated line 911
  65. theorem OAI.CPTSeparation.Grid.grid_connected line 937
  66. theorem OAI.CPTSeparation.Grid.grid_empty_component line 958
  67. theorem OAI.CPTSeparation.Grid.grid_empty_giant line 961
  68. theorem OAI.CPTSeparation.Grid.AtomShift.config_boundary line 975
  69. theorem OAI.CPTSeparation.Grid.quantitative_homogeneity_shift line 981
  70. theorem OAI.CPTSeparation.Grid.central_atomShift line 1039
  71. theorem OAI.CPTSeparation.Grid.quantitative_homogeneity line 1066
  72. theorem OAI.CPTSeparation.Grid.empty_homogeneity line 1076
  73. theorem OAI.CPTSeparation.Counting.Formula.eval_of_partialBijectionSystem line 1087
  74. theorem OAI.CPTSeparation.Grid.boundary_eq_incidence line 1143
  75. def OAI.CPTSeparation.Grid.GiantBound line 1146
  76. theorem OAI.CPTSeparation.Grid.giant_exists_of_bound line 1149
  77. theorem OAI.CPTSeparation.Grid.defect_transport line 1164
  78. def OAI.CPTSeparation.Grid.CompatibleAssignment line 1177
  79. theorem OAI.CPTSeparation.Grid.CompatibleAssignment.mono line 1183
  80. theorem OAI.CPTSeparation.Grid.CompatibleAssignment.extend line 1189
  81. theorem OAI.CPTSeparation.Grid.base_equivalence_numeric line 1238