OAI/Geometry/CAT0Fillings/Tangent/Coordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.ChartGeometry.atlasParam line 16
2. def OAI.CAT0Fillings.ChartGeometry.atlasDomain line 17
3. lemma OAI.CAT0Fillings.ChartGeometry.measurable_atlasParam line 19
4. lemma OAI.CAT0Fillings.ChartGeometry.measurableSet_atlasDomain line 22
5. lemma OAI.CAT0Fillings.ChartGeometry.ae_mem_atlasDomain line 33
6. lemma OAI.CAT0Fillings.ChartGeometry.measurableEmbedding_atlas line 39
7. lemma OAI.CAT0Fillings.ChartGeometry.map_atlasMeasure line 59
8. lemma OAI.CAT0Fillings.ChartGeometry.map_coordinateMeasure_le line 77
9. lemma OAI.CAT0Fillings.ChartGeometry.lintegral_coordinate_le line 82
10. lemma OAI.CAT0Fillings.TangentDensity.lintegral_affine line 103