OAI/LinearAlgebra/MatrixFields/Construction/ShapeEncoding.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeTotal line 16
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.ShapeBounded line 18
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encodeShape line 20
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.decodeShape line 24
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.decode_encodeShape line 27
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encodeShape_side line 32
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.decodeShape_bounded line 36
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encode_decodeShape line 42
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encodeShape_inj line 49
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encodeShape_injective line 53
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encodeShape_total line 59
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalShape line 63
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalShape_source line 66
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalShape_bounded line 70
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalShape_le line 74
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalShape_complement line 78
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalShape_total line 82
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalShape_injective line 87
  19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encodePhysicalShape line 93
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.decode_encodePhysicalShape line 96
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encodePhysicalShape_side line 101
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encodePhysicalShape_inj line 106
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.encodePhysicalShape_total line 111
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.mem_shapes_total line 117
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.coordinate_le_total line 123
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.mem_shapes_bound line 132
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.mem_shapes_bounded line 135
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.below_mem_shapes line 138
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.below_total line 141
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.below_le line 144
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.below_bounded line 154
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.complement_bounded line 157
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.complement_total line 160
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.root_shape_spec line 168
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.root_shapes_nodup line 173
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageA_below_nodup line 175
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageB_below_nodup line 178
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageA_get_injective line 181
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageB_get_injective line 185
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.positiveInitial_shape_spec line 189
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.positiveSecond_shape_spec line 193
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageA_shape_spec line 198
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageA_complement_spec line 203
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageB_shape_spec line 209
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageB_complement_spec line 214
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageC_shape_spec line 220
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageC_complement_spec line 226