OAI/NumberTheory/Catalan/Energy/BarrierTwoNormVPrefix225.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.barrierV2_norm_term_193 line 11
  2. theorem OAI.InternalCatalan.barrierV2_norm_term_194 line 35
  3. theorem OAI.InternalCatalan.barrierV2_norm_term_195 line 60
  4. theorem OAI.InternalCatalan.barrierV2_norm_term_196 line 85
  5. theorem OAI.InternalCatalan.barrierV2_norm_term_197 line 109
  6. theorem OAI.InternalCatalan.barrierV2_norm_term_198 line 133
  7. theorem OAI.InternalCatalan.barrierV2_norm_term_199 line 158
  8. theorem OAI.InternalCatalan.barrierV2_norm_term_200 line 183
  9. theorem OAI.InternalCatalan.barrierV2_norm_block_200 line 207
  10. theorem OAI.InternalCatalan.barrierV2_norm_prefix_200 line 215
  11. theorem OAI.InternalCatalan.barrierV2_norm_term_201 line 238
  12. theorem OAI.InternalCatalan.barrierV2_norm_term_202 line 262
  13. theorem OAI.InternalCatalan.barrierV2_norm_term_203 line 287
  14. theorem OAI.InternalCatalan.barrierV2_norm_term_204 line 312
  15. theorem OAI.InternalCatalan.barrierV2_norm_term_205 line 336
  16. theorem OAI.InternalCatalan.barrierV2_norm_term_206 line 360
  17. theorem OAI.InternalCatalan.barrierV2_norm_term_207 line 385
  18. theorem OAI.InternalCatalan.barrierV2_norm_term_208 line 410
  19. theorem OAI.InternalCatalan.barrierV2_norm_block_208 line 434
  20. theorem OAI.InternalCatalan.barrierV2_norm_prefix_208 line 442
  21. theorem OAI.InternalCatalan.barrierV2_norm_term_209 line 465
  22. theorem OAI.InternalCatalan.barrierV2_norm_term_210 line 489
  23. theorem OAI.InternalCatalan.barrierV2_norm_term_211 line 514
  24. theorem OAI.InternalCatalan.barrierV2_norm_term_212 line 539
  25. theorem OAI.InternalCatalan.barrierV2_norm_term_213 line 563
  26. theorem OAI.InternalCatalan.barrierV2_norm_term_214 line 587
  27. theorem OAI.InternalCatalan.barrierV2_norm_term_215 line 612
  28. theorem OAI.InternalCatalan.barrierV2_norm_term_216 line 637
  29. theorem OAI.InternalCatalan.barrierV2_norm_block_216 line 661
  30. theorem OAI.InternalCatalan.barrierV2_norm_prefix_216 line 669
  31. theorem OAI.InternalCatalan.barrierV2_norm_term_217 line 692
  32. theorem OAI.InternalCatalan.barrierV2_norm_term_218 line 716
  33. theorem OAI.InternalCatalan.barrierV2_norm_term_219 line 741
  34. theorem OAI.InternalCatalan.barrierV2_norm_term_220 line 766
  35. theorem OAI.InternalCatalan.barrierV2_norm_term_221 line 790
  36. theorem OAI.InternalCatalan.barrierV2_norm_term_222 line 814
  37. theorem OAI.InternalCatalan.barrierV2_norm_term_223 line 839
  38. theorem OAI.InternalCatalan.barrierV2_norm_term_224 line 864
  39. theorem OAI.InternalCatalan.barrierV2_norm_block_224 line 888
  40. theorem OAI.InternalCatalan.barrierV2_norm_prefix_224 line 896
  41. theorem OAI.InternalCatalan.barrierV2_norm_term_225 line 919
  42. theorem OAI.InternalCatalan.barrierV2_norm_block_225 line 943
  43. theorem OAI.InternalCatalan.barrierV2_norm_prefix_225 line 951