OAI/Geometry/TamingCompatibility/Charts/ChartComponent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.ManifoldLocalization.chartComponent line 19
2. def OAI.TamingCompatibility.ManifoldLocalization.chartRecover line 23
3. lemma OAI.TamingCompatibility.ManifoldLocalization.chartRecover_apply line 32
4. lemma OAI.TamingCompatibility.ManifoldLocalization.chartRecover_distribution line 41
5. lemma OAI.TamingCompatibility.ManifoldLocalization.chartRecover_inclusion line 64
6. lemma OAI.TamingCompatibility.ManifoldLocalization.localizedLinear_zero_off line 71
7. lemma OAI.TamingCompatibility.ManifoldLocalization.chart_restore line 85
8. lemma OAI.TamingCompatibility.ManifoldLocalization.chartComponent_compact line 108
9. lemma OAI.TamingCompatibility.ManifoldLocalization.h1ToL2_compact line 128