OAI/Analysis/BiholderTransport/CostGeometry/UniformLocalGap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.WeakMTW.uniform_local_scaled_gap line 22
2. lemma OAI.WeakMTWTransport.WeakMTW.uniform_graph_fiber_separation line 94
3. lemma OAI.WeakMTWTransport.graphProjection_base_dist line 122
4. lemma OAI.WeakMTWTransport.WeakMTW.exists_short_injective_graphProjection line 130