OAI/ModelTheory/Choiceless/Support.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CPTSeparation.Support.Scalar line 9
  2. abbrev OAI.CPTSeparation.Support.Plane line 11
  3. def OAI.CPTSeparation.Support.omega line 13
  4. theorem OAI.CPTSeparation.Support.omega_self line 15
  5. theorem OAI.CPTSeparation.Support.omega_zero_left line 17
  6. theorem OAI.CPTSeparation.Support.omega_zero_right line 19
  7. theorem OAI.CPTSeparation.Support.omega_add_left line 21
  8. theorem OAI.CPTSeparation.Support.omega_add_right line 24
  9. theorem OAI.CPTSeparation.Support.omega_neg_left line 27
  10. theorem OAI.CPTSeparation.Support.omega_neg_right line 30
  11. theorem OAI.CPTSeparation.Support.omega_swap line 33
  12. theorem OAI.CPTSeparation.Support.omega_smul_left line 36
  13. theorem OAI.CPTSeparation.Support.omega_smul_right line 39
  14. def OAI.CPTSeparation.Support.correction line 44
  15. theorem OAI.CPTSeparation.Support.correction_self line 47
  16. theorem OAI.CPTSeparation.Support.correction_zero_left line 50
  17. theorem OAI.CPTSeparation.Support.correction_zero_right line 53
  18. theorem OAI.CPTSeparation.Support.correction_add_left line 56
  19. theorem OAI.CPTSeparation.Support.correction_add_right line 60
  20. theorem OAI.CPTSeparation.Support.correction_neg_left line 64
  21. theorem OAI.CPTSeparation.Support.correction_neg_right line 68
  22. theorem OAI.CPTSeparation.Support.correction_swap line 72
  23. structure OAI.CPTSeparation.Support.H line 82
  24. instance OAI.CPTSeparation.Support.H.(instance at line 90) line 90
  25. instance OAI.CPTSeparation.Support.H.(instance at line 92) line 92
  26. instance OAI.CPTSeparation.Support.H.(instance at line 95) line 95
  27. theorem OAI.CPTSeparation.Support.H.one_face line 98
  28. theorem OAI.CPTSeparation.Support.H.one_flow line 107
  29. theorem OAI.CPTSeparation.Support.H.mul_face line 115
  30. theorem OAI.CPTSeparation.Support.H.mul_flow line 117
  31. theorem OAI.CPTSeparation.Support.H.inv_face line 121
  32. theorem OAI.CPTSeparation.Support.H.inv_flow line 130
  33. instance OAI.CPTSeparation.Support.H.(instance at line 138) line 138
  34. def OAI.CPTSeparation.Support.H.central line 143
  35. theorem OAI.CPTSeparation.Support.H.central_mul line 145
  36. theorem OAI.CPTSeparation.Support.H.central_zero line 149
  37. theorem OAI.CPTSeparation.Support.H.central_neg line 158
  38. theorem OAI.CPTSeparation.Support.H.central_commute line 167
  39. theorem OAI.CPTSeparation.Support.H.commutator line 171
  40. def OAI.CPTSeparation.Support.H.projectedAddSubgroup line 190
  41. def OAI.CPTSeparation.Support.H.centralAddSubgroup line 200
  42. def OAI.CPTSeparation.Support.H.projected line 212
  43. def OAI.CPTSeparation.Support.H.centralPart line 215
  44. theorem OAI.CPTSeparation.Support.H.mem_projected line 218
  45. theorem OAI.CPTSeparation.Support.H.mem_centralPart line 221
  46. theorem OAI.CPTSeparation.Support.H.commutator_mem_centralPart line 224
  47. theorem OAI.CPTSeparation.Support.H.stabilizer_isotropic line 232
  48. def OAI.CPTSeparation.Support.H.productEquiv line 239
  49. instance OAI.CPTSeparation.Support.H.(instance at line 245) line 245
  50. def OAI.CPTSeparation.Support.H.projectedLift line 248
  51. theorem OAI.CPTSeparation.Support.H.projectedLift_mem line 251
  52. theorem OAI.CPTSeparation.Support.H.projectedLift_face line 254
  53. theorem OAI.CPTSeparation.Support.H.mul_inv_of_face_eq line 257
  54. def OAI.CPTSeparation.Support.H.subgroupEquiv line 263
  55. theorem OAI.CPTSeparation.Support.H.subgroup_card line 296
  56. theorem OAI.CPTSeparation.Support.H.ambient_card line 305
  57. theorem OAI.CPTSeparation.Support.H.subgroup_index line 313
  58. def OAI.CPTSeparation.Support.diagonalForm line 328
  59. theorem OAI.CPTSeparation.Support.diagonalForm_apply line 355
  60. theorem OAI.CPTSeparation.Support.mem_diagonalForm_ker line 358
  61. def OAI.CPTSeparation.Support.diagonalKerEquiv line 390
  62. theorem OAI.CPTSeparation.Support.diagonalForm_finrank_ker line 411
  63. theorem OAI.CPTSeparation.Support.nonzero_blocks_le_codim line 418
  64. abbrev OAI.CPTSeparation.Grid.Scalar line 451
  65. abbrev OAI.CPTSeparation.Grid.Vertex line 453
  66. abbrev OAI.CPTSeparation.Grid.EdgeX line 455
  67. abbrev OAI.CPTSeparation.Grid.EdgeY line 457
  68. abbrev OAI.CPTSeparation.Grid.EdgeZ line 459
  69. abbrev OAI.CPTSeparation.Grid.Edge line 461
  70. abbrev OAI.CPTSeparation.Grid.FaceXY line 463
  71. abbrev OAI.CPTSeparation.Grid.FaceXZ line 465
  72. abbrev OAI.CPTSeparation.Grid.FaceYZ line 467
  73. abbrev OAI.CPTSeparation.Grid.Face line 469
  74. def OAI.CPTSeparation.Grid.ex line 473
  75. def OAI.CPTSeparation.Grid.ey line 475
  76. def OAI.CPTSeparation.Grid.ez line 477
  77. def OAI.CPTSeparation.Grid.tail line 479
  78. def OAI.CPTSeparation.Grid.head line 484
  79. def OAI.CPTSeparation.Grid.boundary line 489
  80. theorem OAI.CPTSeparation.Grid.boundary_single line 494
  81. def OAI.CPTSeparation.Grid.cycle line 505
  82. theorem OAI.CPTSeparation.Grid.boundary_cycle line 513
  83. def OAI.CPTSeparation.Grid.gradient line 519
  84. def OAI.CPTSeparation.Grid.curl line 521
  85. theorem OAI.CPTSeparation.Grid.single_mul_sum line 523
  86. theorem OAI.CPTSeparation.Grid.curl_xy line 530
  87. theorem OAI.CPTSeparation.Grid.curl_xz line 537
  88. theorem OAI.CPTSeparation.Grid.curl_yz line 544
  89. theorem OAI.CPTSeparation.Grid.curl_gradient line 551
  90. theorem OAI.CPTSeparation.Grid.curl_sub line 556
  91. def OAI.CPTSeparation.Grid.prefixSum line 560
  92. theorem OAI.CPTSeparation.Grid.prefix_zero line 563
  93. theorem OAI.CPTSeparation.Grid.prefix_step line 565
  94. def OAI.CPTSeparation.Grid.phi1 line 587
  95. def OAI.CPTSeparation.Grid.residual1 line 590
  96. def OAI.CPTSeparation.Grid.phi2 line 592
  97. def OAI.CPTSeparation.Grid.residual2 line 595
  98. def OAI.CPTSeparation.Grid.phi3 line 598
  99. def OAI.CPTSeparation.Grid.residual line 601
  100. theorem OAI.CPTSeparation.Grid.residual1_x line 604
  101. theorem OAI.CPTSeparation.Grid.residual2_x line 608
  102. theorem OAI.CPTSeparation.Grid.residual2_y line 613
  103. theorem OAI.CPTSeparation.Grid.residual_x line 618
  104. theorem OAI.CPTSeparation.Grid.residual_y line 623
  105. theorem OAI.CPTSeparation.Grid.residual_z line 628
  106. theorem OAI.CPTSeparation.Grid.curl_residual line 633
  107. theorem OAI.CPTSeparation.Grid.residual_as_gradient line 637
  108. theorem OAI.CPTSeparation.Grid.line_constant line 643
  109. theorem OAI.CPTSeparation.Grid.residual_y_witness line 652
  110. theorem OAI.CPTSeparation.Grid.residual_z_witness line 666
  111. def OAI.CPTSeparation.Grid.nonzeroSet line 687
  112. theorem OAI.CPTSeparation.Grid.mem_nonzeroSet line 690
  113. theorem OAI.CPTSeparation.Grid.card_le_product_of_witness line 693
  114. theorem OAI.CPTSeparation.Grid.card_le_two_products_of_witness line 707
  115. def OAI.CPTSeparation.Grid.badXY line 727
  116. def OAI.CPTSeparation.Grid.badXZ line 730
  117. def OAI.CPTSeparation.Grid.badYZ line 733
  118. def OAI.CPTSeparation.Grid.badSlice line 736
  119. theorem OAI.CPTSeparation.Grid.sum_badSlice line 739
  120. theorem OAI.CPTSeparation.Grid.exists_sparse_slice line 743
  121. theorem OAI.CPTSeparation.Grid.count_residual_y line 753
  122. theorem OAI.CPTSeparation.Grid.count_residual_z line 764
  123. theorem OAI.CPTSeparation.Grid.count_curl line 778
  124. theorem OAI.CPTSeparation.Grid.count_residual line 783
  125. theorem OAI.CPTSeparation.Grid.sparse_cochain line 802