OAI/Combinatorics/SumProduct/Alignment/CubeParameter01.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeParameter.realVertex line 27
  2. def OAI.CubeParameter.vertexSet line 29
  3. lemma OAI.CubeParameter.mem_vertexSet line 31
  4. lemma OAI.CubeParameter.vertex_to_set line 34
  5. lemma OAI.CubeParameter.realVertex_set line 39
  6. lemma OAI.CubeParameter.realVertex_degree line 44
  7. lemma OAI.CubeParameter.degree_append line 54
  8. lemma OAI.CubeParameter.degree_parameter_restrict line 62
  9. lemma OAI.CubeParameter.degree_space_restrict line 67
  10. def OAI.CubeParameter.lift line 79
  11. lemma OAI.CubeParameter.lift_degree line 85
  12. lemma OAI.CubeParameter.lift_vertex line 96
  13. lemma OAI.CubeParameter.degree_lift line 107
  14. lemma OAI.CubeParameter.vertexSet_decide line 112
  15. def OAI.CubeParameter.parameterLift line 117
  16. lemma OAI.CubeParameter.parameterLift_degree line 121
  17. lemma OAI.CubeParameter.parameterLift_vertex line 128
  18. lemma OAI.CubeParameter.degree_parameterLift line 135
  19. lemma OAI.CubeParameter.lift_append line 140
  20. def OAI.CubeCoefficients.coefficients line 170
  21. lemma OAI.CubeCoefficients.coefficients_degree line 175
  22. lemma OAI.CubeCoefficients.coefficients_grid_integer line 183
  23. lemma OAI.CubeCoefficients.coefficients_grid_real line 206
  24. def OAI.CubeCoefficients.value line 217
  25. lemma OAI.CubeCoefficients.value_degree line 220
  26. lemma OAI.CubeCoefficients.value_append line 235
  27. lemma OAI.CubeCoefficients.realize_boolean_rational line 239