OAI/Analysis/BiholderTransport/Coordinates/NormalSubdifferential.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.hasFDerivAt_affine_lower_support line 199
2. def OAI.WeakMTWTransport.normalSubdifferential line 212
3. lemma OAI.WeakMTWTransport.convex_normalSubdifferential line 216
4. lemma OAI.WeakMTWTransport.activeLogs_subset_normalSubdifferential line 235
5. lemma OAI.WeakMTWTransport.active_hull_subset_normalSubdifferential line 264