OAI/MathematicalPhysics/Transonic/Certificates/FixedLowMinusPositive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

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