OAI/Geometry/CAT0Fillings/Calculus/Atlas.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChartGeometry.integral_atlas line 14
2. lemma OAI.CAT0Fillings.ChartGeometry.ae_atlas_of_chart line 25
3. lemma OAI.CAT0Fillings.ChartGeometry.ae_gradient_eq line 32
4. lemma OAI.CAT0Fillings.ChartGeometry.ae_gradient_bound line 36
5. lemma OAI.CAT0Fillings.dot_mulVec_sqrt_cross line 49
6. lemma OAI.CAT0Fillings.ChartGeometry.ae_normalizedCovector_inner line 60