OAI/Geometry/Immersion/ClosedSurface/RealModes.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClosedSurfaceR4.RealModes.RVec line 13
  2. abbrev OAI.ClosedSurfaceR4.RealModes.RField line 14
  3. def OAI.ClosedSurfaceR4.RealModes.complexifyCLM line 16
  4. def OAI.ClosedSurfaceR4.RealModes.complexify line 19
  5. lemma OAI.ClosedSurfaceR4.RealModes.complexify_apply line 21
  6. lemma OAI.ClosedSurfaceR4.RealModes.complexify_dot line 23
  7. lemma OAI.ClosedSurfaceR4.RealModes.complexify_gram line 27
  8. def OAI.ClosedSurfaceR4.RealModes.realNormalPart line 31
  9. lemma OAI.ClosedSurfaceR4.RealModes.complexify_normalPart line 37
  10. lemma OAI.ClosedSurfaceR4.RealModes.realNormalPart_perp line 43
  11. lemma OAI.ClosedSurfaceR4.RealModes.coordDeriv_complexify line 53
  12. lemma OAI.ClosedSurfaceR4.RealModes.contDiff_complexify line 59
  13. lemma OAI.ClosedSurfaceR4.RealModes.contDiff_real_coordDeriv line 62
  14. def OAI.ClosedSurfaceR4.RealModes.realSecond line 66
  15. lemma OAI.ClosedSurfaceR4.RealModes.complexify_realSecond line 69
  16. structure OAI.ClosedSurfaceR4.RealModes.RealModeDomain line 79
  17. lemma OAI.ClosedSurfaceR4.RealModes.RealModeDomain.complexDomain line 84
  18. def OAI.ClosedSurfaceR4.RealModes.freeNormal line 96
  19. lemma OAI.ClosedSurfaceR4.RealModes.freeNormal_perp line 99
  20. lemma OAI.ClosedSurfaceR4.RealModes.freeNormal_unit line 104
  21. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_realSecond line 110
  22. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_freeNormal line 120
  23. def OAI.ClosedSurfaceR4.RealModes.freeSeed line 131
  24. lemma OAI.ClosedSurfaceR4.RealModes.freeSeed_isFree line 134
  25. lemma OAI.ClosedSurfaceR4.RealModes.leadingDerivative_freeSeed line 155
  26. theorem OAI.ClosedSurfaceR4.RealModes.freeSeed_zeroPair line 167
  27. theorem OAI.ClosedSurfaceR4.RealModes.finiteMode_mean_identity line 176