OAI/MathematicalPhysics/Transonic/Certificates/FixedLowPlusPositive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

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