OAI/Geometry/CAT0Fillings/Tangent/Transfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.TangentDensity.global_density_bound line 15
2. lemma OAI.CAT0Fillings.TangentDensity.tangent_coefficient_of_bound line 48
3. lemma OAI.CAT0Fillings.ChartGeometry.ae_chart_tangent_density line 79
4. lemma OAI.CAT0Fillings.TangentDensity.ae_map_of_ae_on_embedding line 155
5. lemma OAI.CAT0Fillings.ChartGeometry.ae_current_of_ae_coordinates line 176