OAI/Geometry/CAT0Fillings/Differentiation/HilbertCharts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ae_restrict_of_arbitrarily_large_pieces line 18
2. theorem OAI.CAT0Fillings.MetricDifferentiation.ae_metricSeminorm_parallelogram_on line 50
3. theorem OAI.CAT0Fillings.MetricDifferentiation.ae_metricSeminorm_distance_bound_on line 76
4. def OAI.CAT0Fillings.MetricDifferentiation.HasCenteredMetricDifferentialWithin line 97
5. theorem OAI.CAT0Fillings.MetricDifferentiation.exists_hilbertian_chart_differential line 102