OAI/Geometry/CAT0Fillings/Differentiation/Centered.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.MetricDifferentiation.metricQuotient line 21
2. lemma OAI.CAT0Fillings.MetricDifferentiation.metricQuotient_lipschitz line 24
3. def OAI.CAT0Fillings.MetricDifferentiation.HasCenteredMetricDifferential line 43
4. lemma OAI.CAT0Fillings.MetricDifferentiation.hasCenteredMetricDifferential_of_dense_directions line 46
5. theorem OAI.CAT0Fillings.MetricDifferentiation.ae_hasCenteredMetricDifferential line 90