OAI/MathematicalPhysics/Transonic/Shooting/FiniteProfile.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SepticProfile.SonicShooting.MatchedPair.localProfile line 12
2. lemma OAI.SepticProfile.SonicShooting.MatchedPair.arc_end line 15
3. lemma OAI.SepticProfile.SonicShooting.MatchedPair.inner_end line 22
4. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_eventually_inner line 28
5. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_eventually_germ line 33
6. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_range line 38
7. lemma OAI.SepticProfile.SonicShooting.Family.germArc_derivative line 45
8. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_derivative_near_join line 61
9. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_smooth_at line 73
10. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_equation line 96
11. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_value line 119
12. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_slope line 123
13. lemma OAI.SepticProfile.SonicShooting.MatchedPair.local_unique_sonic line 128