OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOnePointY1.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.barrier_T_3 line 12

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointX0.lean:15 (same declaration text).

  2. theorem OAI.InternalCatalan.barrier_T_4 line 16

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointX0.lean:19 (same declaration text).

  3. theorem OAI.InternalCatalan.barrier_T_5 line 20

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointX0.lean:23 (same declaration text).

  4. theorem OAI.InternalCatalan.barrier_T_6 line 24

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointX0.lean:27 (same declaration text).

  5. theorem OAI.InternalCatalan.barrier_T_7 line 28

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointX0.lean:31 (same declaration text).

  6. theorem OAI.InternalCatalan.barrier_T_8 line 32

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointX0.lean:35 (same declaration text).

  7. def OAI.InternalCatalan.barrierCase1TPExplicit line 36
  8. theorem OAI.InternalCatalan.barrierCase1TP_eq_explicit line 47
  9. def OAI.InternalCatalan.barrierCase1TVExplicit line 54
  10. theorem OAI.InternalCatalan.barrierCase1TV_eq_explicit line 65
  11. def OAI.InternalCatalan.barrierCase1SVExplicit line 72
  12. theorem OAI.InternalCatalan.barrierCase1SV_eq_explicit line 82
  13. def OAI.InternalCatalan.barrierCase1XApproxRat line 96
  14. def OAI.InternalCatalan.barrierCase1YApproxRat line 101
  15. theorem OAI.InternalCatalan.barrierCase1X_approx_error line 105
  16. theorem OAI.InternalCatalan.barrierCase1Y_approx_error line 121
  17. theorem OAI.InternalCatalan.barrierCase1X0_approx_upper line 141
  18. theorem OAI.InternalCatalan.barrierCase1X0_lt line 149
  19. theorem OAI.InternalCatalan.barrierCase1X1_approx_upper line 166
  20. theorem OAI.InternalCatalan.barrierCase1X1_lt line 174
  21. theorem OAI.InternalCatalan.barrierCase1X2_approx_upper line 191
  22. theorem OAI.InternalCatalan.barrierCase1X2_lt line 199
  23. theorem OAI.InternalCatalan.barrierCase1X3_approx_upper line 216
  24. theorem OAI.InternalCatalan.barrierCase1X3_lt line 224
  25. theorem OAI.InternalCatalan.barrierCase1X4_approx_upper line 241
  26. theorem OAI.InternalCatalan.barrierCase1X4_lt line 249
  27. theorem OAI.InternalCatalan.barrierCase1X5_approx_upper line 266
  28. theorem OAI.InternalCatalan.barrierCase1X5_lt line 274
  29. theorem OAI.InternalCatalan.barrierCase1X6_approx_upper line 291
  30. theorem OAI.InternalCatalan.barrierCase1X6_lt line 299
  31. theorem OAI.InternalCatalan.barrierCase1X7_approx_upper line 316
  32. theorem OAI.InternalCatalan.barrierCase1X7_lt line 324
  33. theorem OAI.InternalCatalan.barrierCase1Y0_approx_upper line 341
  34. theorem OAI.InternalCatalan.barrierCase1Y0_lt line 350
  35. theorem OAI.InternalCatalan.barrierCase1Y1_approx_upper line 369
  36. theorem OAI.InternalCatalan.barrierCase1Y1_lt line 377