OAI/Analysis/SymmetricDomains/ContinuousAutTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.Biholomorph.exists_actual_aut_chart_nonzero_translation_jacobian line 46
  2. def OAI.Release061.Biholomorph.autTransport line 73
  3. theorem OAI.Release061.Biholomorph.autTransport_apply line 76
  4. theorem OAI.Release061.Biholomorph.autTransport_one line 80
  5. theorem OAI.Release061.Biholomorph.autTransport_mul line 85
  6. theorem OAI.Release061.Biholomorph.autTransport_inv line 91
  7. theorem OAI.Release061.Biholomorph.autTransport_symm_cancel line 94
  8. theorem OAI.Release061.Biholomorph.continuous_of_joint_evaluation line 102
  9. theorem OAI.Release061.Biholomorph.continuous_joint_evaluation line 111
  10. theorem OAI.Release061.Biholomorph.continuous_joint_inverse_evaluation line 116
  11. theorem OAI.Release061.Biholomorph.continuous_autTransport line 121