OAI/Geometry/KahlerSplitting/Frobenius.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniversalCoverSplitting.exists_normalized_projection_lift line 33
  2. def OAI.UniversalCoverSplitting.InvolutiveProjectionOn line 110
  3. theorem OAI.UniversalCoverSplitting.normalized_lift_commutes line 115
  4. theorem OAI.UniversalCoverSplitting.exists_normalized_commuting_frame line 154
  5. theorem OAI.UniversalCoverSplitting.CommutingFlowData.fderiv_initial_zero line 197
  6. theorem OAI.UniversalCoverSplitting.CommutingFlowData.fderiv_time_sum line 213
  7. theorem OAI.UniversalCoverSplitting.CommutingFlowData.fderiv_base line 222
  8. theorem OAI.UniversalCoverSplitting.transverse_flow_hasFDerivAt line 232
  9. abbrev OAI.UniversalCoverSplitting.transverseFlowParameter line 276
  10. def OAI.UniversalCoverSplitting.transverseFlowLinear line 279
  11. theorem OAI.UniversalCoverSplitting.transverseFlowParameter_hasFDerivAt line 285
  12. theorem OAI.UniversalCoverSplitting.transverseFlow_time line 291
  13. theorem OAI.UniversalCoverSplitting.exists_holomorphic_ift_chart line 314
  14. theorem OAI.UniversalCoverSplitting.chart_fderiv_inverse line 352
  15. theorem OAI.UniversalCoverSplitting.chart_kernel_eq_projection line 374
  16. theorem OAI.UniversalCoverSplitting.foliation_chart_from_flows line 411
  17. theorem OAI.UniversalCoverSplitting.exists_projection_coordinates line 474