OAI/Geometry/TamingCompatibility/Hodge/HodgeNormalInverse.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.inverseRegularDomain line 17
  2. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.inverseRegularDomain_open line 21
  3. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.inverseRegularDomain_smooth line 28
  4. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.geometricNormalChart line 51
  5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.geometricNormalChart_apply line 54
  6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.geometricNormalChart_smooth line 57
  7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.geometricNormalChart_center line 61
  8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.geometricNormalChart_symm_fst line 71
  9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.geometricNormalChart_symm_right line 78
  10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.geometricNormalChart_symm_left line 87
  11. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.inverseDisplacement line 112
  12. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.inverseTubeDomain line 115
  13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.inverseTubeDomain_open line 120
  14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.inverseTubeDomain_center line 126
  15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.inverseDisplacement_smooth line 131
  16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.inverseDisplacement_zero line 140
  17. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.inverseDisplacement_right line 146
  18. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.exists_inverse_center_ball line 151
  19. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.inverseDisplacement_bound line 165