OAI/Geometry/TamingCompatibility/Charts/Coordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.FiberCoordinates.coordinates line 14
  2. lemma OAI.TamingCompatibility.FiberCoordinates.coordinates_apply line 20
  3. lemma OAI.TamingCompatibility.FiberCoordinates.coordinates_injective line 24
  4. def OAI.TamingCompatibility.FiberCoordinates.complexCoordinates line 31
  5. lemma OAI.TamingCompatibility.FiberCoordinates.complexCoordinates_apply line 37
  6. lemma OAI.TamingCompatibility.FiberCoordinates.complexCoordinates_injective line 41
  7. abbrev OAI.TamingCompatibility.ManifoldLocalization.CoordinateFiber line 55
  8. def OAI.TamingCompatibility.ManifoldLocalization.formCoordinates line 57
  9. def OAI.TamingCompatibility.ManifoldLocalization.localizedLinear line 61
  10. abbrev OAI.TamingCompatibility.ManifoldLocalization.ChartL2 line 77
  11. def OAI.TamingCompatibility.ManifoldLocalization.localizeL2 line 81
  12. lemma OAI.TamingCompatibility.ManifoldLocalization.localizeL2_apply line 88
  13. lemma OAI.TamingCompatibility.ManifoldLocalization.localizeL2_injective line 92
  14. def OAI.TamingCompatibility.ManifoldLocalization.globalL2 line 111
  15. instance OAI.TamingCompatibility.ManifoldLocalization.globalL2_complete line 114
  16. def OAI.TamingCompatibility.ManifoldLocalization.smoothToL2 line 118
  17. lemma OAI.TamingCompatibility.ManifoldLocalization.smoothToL2_injective line 122