OAI/MathematicalPhysics/Transonic/Certificates/FixedHighMinusPositive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SepticProfile.FixedHighMinusPositive.Q line 9
2. def OAI.SepticProfile.FixedHighMinusPositive.r line 10
3. theorem OAI.SepticProfile.FixedHighMinusPositive.Q_pos line 11
4. theorem OAI.SepticProfile.FixedHighMinusPositive.head0 line 12
5. theorem OAI.SepticProfile.FixedHighMinusPositive.head1 line 13
6. theorem OAI.SepticProfile.FixedHighMinusPositive.head2 line 14
7. theorem OAI.SepticProfile.FixedHighMinusPositive.middle line 15
8. theorem OAI.SepticProfile.FixedHighMinusPositive.tail_bound line 17
9. theorem OAI.SepticProfile.FixedHighMinusPositive.finite_positive line 18