OAI/Analysis/BiholderTransport/Geodesics/MetricSegments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.IsMetricChain line 25
2. lemma OAI.WeakMTWTransport.isMetricChain_initial line 30
3. lemma OAI.WeakMTWTransport.IsMetricChain.closure line 48
4. lemma OAI.WeakMTWTransport.exists_maximal_metricChain line 61
5. lemma OAI.WeakMTWTransport.insert_midpoint_metricChain line 83
6. lemma OAI.WeakMTWTransport.maximal_metricChain_full_projection line 135
7. lemma OAI.WeakMTWTransport.exists_metric_segment line 175