OAI/MathematicalPhysics/Transonic/Certificates/FixedHighPlusPositive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

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