OAI/Geometry/TamingCompatibility/Hodge/HodgePatchContinuity.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ManifoldKernelExtension.push_continuous line 15
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gammaLeadingMatrix_continuous line 37
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gammaLeadingPatch_continuous line 79
4. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gammaPatchWedge line 87
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gammaPatchWedge_continuous line 95
6. abbrev OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.UnitPair line 123
7. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularBase line 125
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularBase_continuous line 128
9. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularDomain line 133
10. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularChartCoordinates line 136
11. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularCoordinates line 139
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularDomain_closed line 143
13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularChartCoordinates_mem line 148
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularChartCoordinates_source line 160
15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularCoordinates_mem line 166
16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularCoordinates_chart line 175
17. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularCoordinates_bases line 185
18. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularChartCoordinates_continuousOn line 202
19. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularCoordinates_continuousOn line 211
20. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularWeight line 219
21. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularWeight_nonneg line 225
22. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularWeight_continuousOn line 230
23. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularNearSet line 266
24. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularNearSet_closed line 271
25. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularNear line 278
26. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularNear_nonneg line 282
27. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.angularNear_integrable line 288