OAI/Combinatorics/VariableWL/Affine.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. class OAI.VariableWL.FiniteNumbering line 9
  2. instance OAI.VariableWL.(instance at line 12) line 12
  3. instance OAI.VariableWL.(instance at line 14) line 14
  4. def OAI.VariableWL.enumeration line 17
  5. abbrev OAI.VariableWL.Affine.Bit line 23
  6. abbrev OAI.VariableWL.Affine.Vec line 24
  7. abbrev OAI.VariableWL.Affine.SquareVal line 25
  8. def OAI.VariableWL.Affine.boundary line 31
  9. def OAI.VariableWL.Affine.Fiber line 35
  10. theorem OAI.VariableWL.Affine.boundary_add line 38
  11. theorem OAI.VariableWL.Affine.boundary_zero line 43
  12. def OAI.VariableWL.Affine.kernel line 47
  13. theorem OAI.VariableWL.Affine.fiber_nonempty line 65
  14. theorem OAI.VariableWL.Affine.fiber_translate line 69
  15. theorem OAI.VariableWL.Affine.fiber_full_left line 87
  16. theorem OAI.VariableWL.Affine.fiber_full_right line 92
  17. theorem OAI.VariableWL.Affine.fiber_full_vertical₀ line 97
  18. theorem OAI.VariableWL.Affine.fiber_full_vertical₁ line 102
  19. def OAI.VariableWL.Affine.fiberEquiv line 107
  20. theorem OAI.VariableWL.Affine.fiber_card line 123
  21. theorem OAI.VariableWL.Affine.fiber_card_le_sixteen line 128
  22. abbrev OAI.VariableWL.Markers.Bit line 139
  23. def OAI.VariableWL.Markers.walkSum line 144
  24. theorem OAI.VariableWL.Markers.walkSum_nil line 148
  25. theorem OAI.VariableWL.Markers.walkSum_cons line 151
  26. theorem OAI.VariableWL.Markers.walkSum_append line 155
  27. theorem OAI.VariableWL.Markers.walkSum_reverse line 162
  28. theorem OAI.VariableWL.Markers.exists_potential line 172
  29. theorem OAI.VariableWL.Markers.walkSum_of_potential line 190
  30. theorem OAI.VariableWL.Affine.gauge_horizontal line 204
  31. theorem OAI.VariableWL.Affine.gauge_vertical line 214
  32. theorem OAI.VariableWL.Affine.shift_difference line 224
  33. abbrev OAI.VariableWL.ScalarImages.Bit line 236
  34. abbrev OAI.VariableWL.ScalarImages.Pair line 237
  35. def OAI.VariableWL.ScalarImages.sum line 239
  36. def OAI.VariableWL.ScalarImages.buffer line 241
  37. theorem OAI.VariableWL.ScalarImages.buffer_nonempty line 245
  38. theorem OAI.VariableWL.ScalarImages.buffer_image_sum line 249
  39. theorem OAI.VariableWL.ScalarImages.buffer_image_fst line 257
  40. theorem OAI.VariableWL.ScalarImages.buffer_image_snd line 265
  41. theorem OAI.VariableWL.ScalarImages.zero_buffer_unique line 273
  42. theorem OAI.VariableWL.ScalarImages.zero_propagates line 284
  43. def OAI.VariableWL.ScalarImages.andWitness line 290
  44. theorem OAI.VariableWL.ScalarImages.andWitness_nonempty line 293
  45. theorem OAI.VariableWL.ScalarImages.andWitness_fst line 296
  46. theorem OAI.VariableWL.ScalarImages.andWitness_snd line 305
  47. theorem OAI.VariableWL.ScalarImages.andWitness_sum line 314