OAI/Geometry/TamingCompatibility/Charts/FiniteCharts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.TamingCompatibility.ManifoldLocalization.FiniteCharts line 25
2. theorem OAI.TamingCompatibility.ManifoldLocalization.finiteCharts_nonempty line 31
3. def OAI.TamingCompatibility.ManifoldLocalization.finiteCharts line 47
4. lemma OAI.TamingCompatibility.ManifoldLocalization.partition_sum line 52
5. def OAI.TamingCompatibility.ManifoldLocalization.coordinateSupport line 55
6. lemma OAI.TamingCompatibility.ManifoldLocalization.coordinateSupport_compact line 59
7. lemma OAI.TamingCompatibility.ManifoldLocalization.coordinateSupport_subset line 64
8. lemma OAI.TamingCompatibility.ManifoldLocalization.smooth_indicator_of_compact line 73
9. def OAI.TamingCompatibility.ManifoldLocalization.localizedFunction line 96
10. lemma OAI.TamingCompatibility.ManifoldLocalization.localizedFunction_smooth_compact line 103
11. def OAI.TamingCompatibility.ManifoldLocalization.localizedSchwartz line 121
12. lemma OAI.TamingCompatibility.ManifoldLocalization.localizedFunction_add line 128
13. lemma OAI.TamingCompatibility.ManifoldLocalization.localizedFunction_smul line 138
14. lemma OAI.TamingCompatibility.ManifoldLocalization.localizedFunction_zero line 149
15. lemma OAI.TamingCompatibility.ManifoldLocalization.eq_zero_of_localizedFunction_eq_zero line 155