OAI/Geometry/TamingCompatibility/Charts/RadialUnitCoordinates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitChartDomain line 18
2. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitChartBase line 21
3. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitChartVector line 24
4. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitChartDomain_closed line 28
5. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitChart_mem line 35
6. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitChartBase_continuousOn line 45
7. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitChartVector_continuousOn line 54
8. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitChart_eval line 66
9. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitRadialDefect line 89
10. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitRadialRadius line 93
11. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitRadialDefect_continuousOn line 97
12. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitRadialRadius_continuousOn line 108
13. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitRadialDefect_nonneg line 115