OAI/Geometry/IsometricImmersion/LocalDomains.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.openDomainExtend line 16
  2. theorem OAI.SmoothLocal.Geometry.openDomainExtend_apply line 19
  3. theorem OAI.SmoothLocal.Geometry.openDomainExtend_restrict line 23
  4. theorem OAI.SmoothLocal.Geometry.contMDiff_restrict_iff line 30
  5. theorem OAI.SmoothLocal.Geometry.openDomainExtend_contDiffOn line 42
  6. theorem OAI.SmoothLocal.Geometry.mfderiv_restrict_eq_fderiv line 50
  7. theorem OAI.SmoothLocal.Geometry.fderiv_openDomainExtend_eq_mfderiv line 71
  8. def OAI.SmoothLocal.Geometry.LocalIsometric line 83
  9. theorem OAI.SmoothLocal.Geometry.localIsometric_restrict_iff line 90
  10. theorem OAI.SmoothLocal.Geometry.localIsometric_extend_iff line 110
  11. theorem OAI.SmoothLocal.Geometry.localIsometric_injective_differential line 115
  12. def OAI.SmoothLocal.Geometry.LocalSmoothPositive line 122

    Also declared: ComparatorChallenges/IsometricImmersion.lean:21 (same declaration text).

  13. theorem OAI.SmoothLocal.Geometry.localSmoothPositive_restrict_iff line 127
  14. theorem OAI.SmoothLocal.Geometry.localSmoothPositive_extend_iff line 137