OAI/MathematicalPhysics/Transonic/Certificates/Parameters47.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SepticProfile.ExteriorCertificates.C47.lo line 10
  2. def OAI.SepticProfile.ExteriorCertificates.C47.hi line 11
  3. theorem OAI.SepticProfile.ExteriorCertificates.C47.qpos line 12
  4. theorem OAI.SepticProfile.ExteriorCertificates.C47.lo_mem line 13
  5. theorem OAI.SepticProfile.ExteriorCertificates.C47.hi_mem line 14
  6. theorem OAI.SepticProfile.ExteriorCertificates.C47.sig_lo line 15
  7. theorem OAI.SepticProfile.ExteriorCertificates.C47.sig_hi line 16
  8. theorem OAI.SepticProfile.ExteriorCertificates.C47.sig_mem line 17
  9. theorem OAI.SepticProfile.ExteriorCertificates.C47.kap_lo line 20
  10. theorem OAI.SepticProfile.ExteriorCertificates.C47.kap_hi line 21
  11. theorem OAI.SepticProfile.ExteriorCertificates.C47.kap_mem line 22
  12. theorem OAI.SepticProfile.ExteriorCertificates.C47.s_lo line 25
  13. theorem OAI.SepticProfile.ExteriorCertificates.C47.s_hi line 26
  14. theorem OAI.SepticProfile.ExteriorCertificates.C47.s_mem line 27
  15. theorem OAI.SepticProfile.ExteriorCertificates.C47.rho_lo line 30
  16. theorem OAI.SepticProfile.ExteriorCertificates.C47.rho_hi line 31
  17. theorem OAI.SepticProfile.ExteriorCertificates.C47.rho_mem line 32
  18. theorem OAI.SepticProfile.ExteriorCertificates.C47.weights_eq line 35
  19. theorem OAI.SepticProfile.ExteriorCertificates.C47.st_eq line 36
  20. theorem OAI.SepticProfile.ExteriorCertificates.C47.L0_eq line 37
  21. theorem OAI.SepticProfile.ExteriorCertificates.C47.b1_eq line 38
  22. theorem OAI.SepticProfile.ExteriorCertificates.C47.den2 line 39
  23. theorem OAI.SepticProfile.ExteriorCertificates.C47.den3 line 40
  24. theorem OAI.SepticProfile.ExteriorCertificates.C47.den4 line 41
  25. theorem OAI.SepticProfile.ExteriorCertificates.C47.den5 line 42
  26. theorem OAI.SepticProfile.ExteriorCertificates.C47.den6 line 43
  27. theorem OAI.SepticProfile.ExteriorCertificates.C47.den7 line 44
  28. theorem OAI.SepticProfile.ExteriorCertificates.C47.den8 line 45
  29. theorem OAI.SepticProfile.ExteriorCertificates.C47.den9 line 46
  30. theorem OAI.SepticProfile.ExteriorCertificates.C47.den10 line 47
  31. theorem OAI.SepticProfile.ExteriorCertificates.C47.den11 line 48
  32. theorem OAI.SepticProfile.ExteriorCertificates.C47.den12 line 49
  33. theorem OAI.SepticProfile.ExteriorCertificates.C47.den13 line 50
  34. theorem OAI.SepticProfile.ExteriorCertificates.C47.den14 line 51
  35. theorem OAI.SepticProfile.ExteriorCertificates.C47.den15 line 52
  36. theorem OAI.SepticProfile.ExteriorCertificates.C47.den16 line 53
  37. theorem OAI.SepticProfile.ExteriorCertificates.C47.den17 line 54
  38. theorem OAI.SepticProfile.ExteriorCertificates.C47.den18 line 55
  39. theorem OAI.SepticProfile.ExteriorCertificates.C47.den19 line 56
  40. theorem OAI.SepticProfile.ExteriorCertificates.C47.den20 line 57
  41. theorem OAI.SepticProfile.ExteriorCertificates.C47.den21 line 58
  42. theorem OAI.SepticProfile.ExteriorCertificates.C47.den22 line 59
  43. theorem OAI.SepticProfile.ExteriorCertificates.C47.den23 line 60
  44. theorem OAI.SepticProfile.ExteriorCertificates.C47.den24 line 61
  45. theorem OAI.SepticProfile.ExteriorCertificates.C47.den25 line 62
  46. theorem OAI.SepticProfile.ExteriorCertificates.C47.den26 line 63
  47. theorem OAI.SepticProfile.ExteriorCertificates.C47.den27 line 64
  48. theorem OAI.SepticProfile.ExteriorCertificates.C47.den28 line 65
  49. theorem OAI.SepticProfile.ExteriorCertificates.C47.den29 line 66
  50. theorem OAI.SepticProfile.ExteriorCertificates.C47.den30 line 67
  51. theorem OAI.SepticProfile.ExteriorCertificates.C47.den31 line 68
  52. theorem OAI.SepticProfile.ExteriorCertificates.C47.den32 line 69
  53. theorem OAI.SepticProfile.ExteriorCertificates.C47.den33 line 70
  54. theorem OAI.SepticProfile.ExteriorCertificates.C47.den34 line 71
  55. theorem OAI.SepticProfile.ExteriorCertificates.C47.den35 line 72
  56. theorem OAI.SepticProfile.ExteriorCertificates.C47.den36 line 73
  57. theorem OAI.SepticProfile.ExteriorCertificates.C47.den37 line 74
  58. theorem OAI.SepticProfile.ExteriorCertificates.C47.den38 line 75
  59. theorem OAI.SepticProfile.ExteriorCertificates.C47.den39 line 76
  60. theorem OAI.SepticProfile.ExteriorCertificates.C47.den40 line 77
  61. theorem OAI.SepticProfile.ExteriorCertificates.C47.den41 line 78
  62. theorem OAI.SepticProfile.ExteriorCertificates.C47.den42 line 79
  63. theorem OAI.SepticProfile.ExteriorCertificates.C47.den43 line 80
  64. theorem OAI.SepticProfile.ExteriorCertificates.C47.den44 line 81
  65. theorem OAI.SepticProfile.ExteriorCertificates.C47.den45 line 82
  66. theorem OAI.SepticProfile.ExteriorCertificates.C47.den46 line 83
  67. theorem OAI.SepticProfile.ExteriorCertificates.C47.den47 line 84
  68. theorem OAI.SepticProfile.ExteriorCertificates.C47.den48 line 85
  69. theorem OAI.SepticProfile.ExteriorCertificates.C47.den49 line 86
  70. theorem OAI.SepticProfile.ExteriorCertificates.C47.den50 line 87
  71. theorem OAI.SepticProfile.ExteriorCertificates.C47.den51 line 88
  72. theorem OAI.SepticProfile.ExteriorCertificates.C47.den52 line 89
  73. theorem OAI.SepticProfile.ExteriorCertificates.C47.den53 line 90
  74. theorem OAI.SepticProfile.ExteriorCertificates.C47.den54 line 91
  75. theorem OAI.SepticProfile.ExteriorCertificates.C47.den55 line 92
  76. theorem OAI.SepticProfile.ExteriorCertificates.C47.den56 line 93
  77. theorem OAI.SepticProfile.ExteriorCertificates.C47.den57 line 94
  78. theorem OAI.SepticProfile.ExteriorCertificates.C47.den58 line 95
  79. theorem OAI.SepticProfile.ExteriorCertificates.C47.den59 line 96
  80. theorem OAI.SepticProfile.ExteriorCertificates.C47.den60 line 97
  81. theorem OAI.SepticProfile.ExteriorCertificates.C47.den61 line 98
  82. theorem OAI.SepticProfile.ExteriorCertificates.C47.den62 line 99
  83. theorem OAI.SepticProfile.ExteriorCertificates.C47.den63 line 100
  84. theorem OAI.SepticProfile.ExteriorCertificates.C47.den64 line 101
  85. theorem OAI.SepticProfile.ExteriorCertificates.C47.den65 line 102
  86. theorem OAI.SepticProfile.ExteriorCertificates.C47.den66 line 103
  87. theorem OAI.SepticProfile.ExteriorCertificates.C47.den67 line 104
  88. theorem OAI.SepticProfile.ExteriorCertificates.C47.den68 line 105
  89. theorem OAI.SepticProfile.ExteriorCertificates.C47.den69 line 106
  90. theorem OAI.SepticProfile.ExteriorCertificates.C47.den70 line 107
  91. theorem OAI.SepticProfile.ExteriorCertificates.C47.den71 line 108
  92. theorem OAI.SepticProfile.ExteriorCertificates.C47.den72 line 109
  93. theorem OAI.SepticProfile.ExteriorCertificates.C47.den73 line 110
  94. theorem OAI.SepticProfile.ExteriorCertificates.C47.den74 line 111
  95. theorem OAI.SepticProfile.ExteriorCertificates.C47.den_eq line 112
  96. theorem OAI.SepticProfile.ExteriorCertificates.C47.num74_pos line 187