OAI/Analysis/HenonEmden/LineCoordinates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HenonLaneEmden.LineCoordinates.transverse line 16
  2. lemma OAI.HenonLaneEmden.LineCoordinates.norm_unit line 18
  3. lemma OAI.HenonLaneEmden.LineCoordinates.inner_transverse line 20
  4. def OAI.HenonLaneEmden.LineCoordinates.join line 23
  5. lemma OAI.HenonLaneEmden.LineCoordinates.join_surjective line 37
  6. def OAI.HenonLaneEmden.LineCoordinates.isometry line 47
  7. lemma OAI.HenonLaneEmden.LineCoordinates.isometry_apply line 50
  8. lemma OAI.HenonLaneEmden.LineCoordinates.norm_join_sq line 53
  9. def OAI.HenonLaneEmden.LineCoordinates.measurableEquiv line 61
  10. lemma OAI.HenonLaneEmden.LineCoordinates.measurableEquiv_apply line 64
  11. lemma OAI.HenonLaneEmden.LineCoordinates.measurePreserving line 67
  12. lemma OAI.HenonLaneEmden.LineCoordinates.continuous_measurableEquiv line 71
  13. lemma OAI.HenonLaneEmden.LineCoordinates.distance_sq line 75
  14. lemma OAI.HenonLaneEmden.LineCoordinates.parallel line 82
  15. lemma OAI.HenonLaneEmden.LineCoordinates.transverse_nontrivial line 87