OAI/Analysis/BiholderTransport/Coordinates/NormalEikonal.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.WeakMTWTransport.doubleNormalCostline 23 - lemma
OAI.WeakMTWTransport.doubleNormalCost_contDiffAtline 27 - lemma
OAI.WeakMTWTransport.exists_normal_eikonal_logline 48