OAI/Geometry/CylinderCovering/Rational/Similarity.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalSimilarity.h_pos line 10
  2. lemma OAI.RationalSimilarity.ell_pos line 11
  3. lemma OAI.RationalSimilarity.h_ne_zero line 12
  4. lemma OAI.RationalSimilarity.ell_ne_zero line 13
  5. lemma OAI.RationalSimilarity.h_sq line 14
  6. lemma OAI.RationalSimilarity.ell_eq line 19
  7. lemma OAI.RationalSimilarity.ell_sq line 20
  8. lemma OAI.RationalSimilarity.ell_mul_h line 21
  9. lemma OAI.RationalSimilarity.phi_apply_zero line 23
  10. lemma OAI.RationalSimilarity.phi_apply_one line 24
  11. lemma OAI.RationalSimilarity.phi_apply_two line 25
  12. lemma OAI.RationalSimilarity.phi_decomposition line 27
  13. lemma OAI.RationalSimilarity.reflection_isometry line 33
  14. lemma OAI.RationalSimilarity.phi_dist line 41
  15. lemma OAI.RationalSimilarity.phi_membership line 46
  16. lemma OAI.RationalSimilarity.phi_surjective line 74
  17. theorem OAI.RationalSimilarity.phi_image_tetrahedron line 80
  18. lemma OAI.RationalSimilarity.shifted_reflection_isometry line 90
  19. theorem OAI.RationalSimilarity.phi_euclideanHausdorffMeasure line 96
  20. theorem OAI.RationalSimilarity.phi_area line 109