OAI/Geometry/KahlerSplitting/ClosedForm.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalCoverSplitting.alternatingBilinear line 34
  2. theorem OAI.UniversalCoverSplitting.alternatingBilinear_apply line 38
  3. theorem OAI.UniversalCoverSplitting.alternatingBilinear_contDiff line 44
  4. theorem OAI.UniversalCoverSplitting.KahlerMetric.skew_I line 54
  5. theorem OAI.UniversalCoverSplitting.KahlerMetric.skew_fundamentalInChart line 61
  6. def OAI.UniversalCoverSplitting.kahlerFormInChart line 70
  7. theorem OAI.UniversalCoverSplitting.kahlerFormInChart_apply line 75
  8. theorem OAI.UniversalCoverSplitting.KahlerMetric.smooth_formInChart line 84
  9. theorem OAI.UniversalCoverSplitting.KahlerMetric.closed_formInChart line 95
  10. theorem OAI.UniversalCoverSplitting.continuousOn_cauchy_partial line 122
  11. theorem OAI.UniversalCoverSplitting.continuousAt_partial_deriv line 155
  12. def OAI.UniversalCoverSplitting.totalPartialDeriv line 175
  13. theorem OAI.UniversalCoverSplitting.hasStrictFDerivAt_of_continuousOn_of_separately line 181
  14. theorem OAI.UniversalCoverSplitting.differentiableOn_of_continuousOn_of_separately line 209
  15. theorem OAI.UniversalCoverSplitting.continuousAt_totalPartialDeriv line 219
  16. theorem OAI.UniversalCoverSplitting.continuousAt_fderiv_twoDim_prod line 236
  17. theorem OAI.UniversalCoverSplitting.continuousOn_fderiv_twoDim line 254