OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointData.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.Case2PointData.X0 line 9
  2. def OAI.InternalCatalan.Case2PointData.X1 line 11
  3. def OAI.InternalCatalan.Case2PointData.X2 line 13
  4. def OAI.InternalCatalan.Case2PointData.X3 line 15
  5. def OAI.InternalCatalan.Case2PointData.X4 line 17
  6. def OAI.InternalCatalan.Case2PointData.X5 line 19
  7. def OAI.InternalCatalan.Case2PointData.X6 line 21
  8. def OAI.InternalCatalan.Case2PointData.X7 line 23
  9. def OAI.InternalCatalan.Case2PointData.X8 line 25
  10. def OAI.InternalCatalan.Case2PointData.X9 line 27
  11. def OAI.InternalCatalan.Case2PointData.X10 line 29
  12. def OAI.InternalCatalan.Case2PointData.X11 line 31
  13. def OAI.InternalCatalan.Case2PointData.X12 line 33
  14. def OAI.InternalCatalan.Case2PointData.X13 line 35
  15. def OAI.InternalCatalan.Case2PointData.X14 line 37
  16. def OAI.InternalCatalan.Case2PointData.X15 line 39
  17. def OAI.InternalCatalan.Case2PointData.X16 line 41
  18. def OAI.InternalCatalan.Case2PointData.X17 line 43
  19. def OAI.InternalCatalan.Case2PointData.X18 line 45
  20. def OAI.InternalCatalan.Case2PointData.Y0 line 47
  21. def OAI.InternalCatalan.Case2PointData.Y1 line 49
  22. def OAI.InternalCatalan.Case2PointData.Y2 line 51
  23. def OAI.InternalCatalan.Case2PointData.Y3 line 53
  24. def OAI.InternalCatalan.Case2PointData.Y4 line 55
  25. def OAI.InternalCatalan.Case2PointData.Y5 line 57
  26. def OAI.InternalCatalan.Case2PointData.Y6 line 59
  27. def OAI.InternalCatalan.Case2PointData.Y7 line 61
  28. def OAI.InternalCatalan.Case2PointData.Y8 line 63
  29. def OAI.InternalCatalan.Case2PointData.Y9 line 65
  30. def OAI.InternalCatalan.Case2PointData.Y10 line 67
  31. def OAI.InternalCatalan.Case2PointData.Y11 line 69
  32. def OAI.InternalCatalan.Case2PointData.Y12 line 71
  33. def OAI.InternalCatalan.Case2PointData.Y13 line 73
  34. def OAI.InternalCatalan.Case2PointData.Y14 line 75
  35. def OAI.InternalCatalan.Case2PointData.Y15 line 77
  36. def OAI.InternalCatalan.Case2PointData.Y16 line 79
  37. def OAI.InternalCatalan.Case2PointData.Y17 line 81
  38. def OAI.InternalCatalan.Case2PointData.XPoints line 83
  39. theorem OAI.InternalCatalan.Case2PointData.X_points_domain line 86
  40. def OAI.InternalCatalan.Case2PointData.YPoints line 89
  41. theorem OAI.InternalCatalan.Case2PointData.Y_points_domain line 92