OAI/Geometry/KahlerSplitting/CommutingFlows.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalCoverSplitting.FlowTimes line 31
  2. def OAI.UniversalCoverSplitting.trimFlowTimes line 33
  3. theorem OAI.UniversalCoverSplitting.trimFlowTimes_apply line 36
  4. theorem OAI.UniversalCoverSplitting.trimFlowTimes_single_castSucc line 39
  5. theorem OAI.UniversalCoverSplitting.trimFlowTimes_single_last line 44
  6. structure OAI.UniversalCoverSplitting.CommutingFlowData line 49
  7. theorem OAI.UniversalCoverSplitting.exists_commutingFlowData line 65
  8. theorem OAI.UniversalCoverSplitting.continuousOn_directional_cauchy line 156
  9. theorem OAI.UniversalCoverSplitting.continuousAt_directional_fderiv line 186
  10. theorem OAI.UniversalCoverSplitting.finite_holomorphic_contDiffOn_one line 229
  11. def OAI.UniversalCoverSplitting.radialClamp line 247
  12. theorem OAI.UniversalCoverSplitting.continuous_radialClamp line 250
  13. theorem OAI.UniversalCoverSplitting.radialClamp_eq_self_of_mem_closedBall line 258
  14. theorem OAI.UniversalCoverSplitting.radialClamp_mem_closedBall line 263
  15. theorem OAI.UniversalCoverSplitting.radialClamp_eventuallyEq_id line 274
  16. theorem OAI.UniversalCoverSplitting.holomorphic_continuous_representatives line 289
  17. theorem OAI.UniversalCoverSplitting.finite_holomorphic_representatives line 327