OAI/MathematicalPhysics/Transonic/Shooting/MatchedAxisJoin.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SepticProfile.SonicShooting.MatchedPair.axisGerm line 12
2. def OAI.SepticProfile.SonicShooting.MatchedPair.inner line 14
3. lemma OAI.SepticProfile.SonicShooting.MatchedPair.axisGerm_analytic line 16
4. lemma OAI.SepticProfile.SonicShooting.MatchedPair.axisGerm_range line 23
5. lemma OAI.SepticProfile.SonicShooting.MatchedPair.axisGerm_equation line 31
6. lemma OAI.SepticProfile.SonicShooting.MatchedPair.axisGerm_derivative line 39
7. lemma OAI.SepticProfile.SonicShooting.MatchedPair.arc_start line 51
8. lemma OAI.SepticProfile.SonicShooting.MatchedPair.inner_range line 57
9. lemma OAI.SepticProfile.SonicShooting.MatchedPair.inner_derivative line 64
10. lemma OAI.SepticProfile.SonicShooting.MatchedPair.inner_smooth_between line 73
11. lemma OAI.SepticProfile.SonicShooting.MatchedPair.inner_eventually_axis line 80
12. lemma OAI.SepticProfile.SonicShooting.MatchedPair.inner_smooth_at line 85
13. lemma OAI.SepticProfile.SonicShooting.MatchedPair.inner_equation line 94