OAI/Geometry/TamingCompatibility/DifferentialForms/EuclideanAngularDomain.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanNearSet line 20
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanNearSet_closed line 26
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanLine_continuousOn line 33
4. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanAngularWeight line 76
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanAngularWeight_nonneg line 80
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanAngularWeight_continuousOn line 85
7. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanAngularNear line 93
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanAngularNear_nonneg line 97
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanAngularNear_integrable line 101
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.euclideanNear_physical_distance line 129
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.separating_current_euclidean_near_mass line 154