OAI/Analysis/BiholderTransport/Contact/GraphProjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.subgradientGraph line 240
2. def OAI.WeakMTWTransport.graphProjection line 243
3. lemma OAI.WeakMTWTransport.continuous_graphProjection line 251
4. lemma OAI.WeakMTWTransport.WeakMTW.isOpenMap_graphProjection line 257
5. lemma OAI.WeakMTWTransport.global_min_divided_cost_subgradient line 287
6. lemma OAI.WeakMTWTransport.surjective_graphProjection line 321