OAI/Geometry/CylinderCovering/Convexity/AffineSimplexChord.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimplexChord.coord_add_smul line 12
  2. theorem OAI.SimplexChord.sum_coord_linear_eq_zero line 19
  3. theorem OAI.SimplexChord.coord_linear_ne_zero line 30
  4. theorem OAI.SimplexChord.mem_convexHull_iff_coord_mem line 43
  5. theorem OAI.SimplexChord.exists_point_with_coords line 49
  6. theorem OAI.SimplexChord.affine_endpoints_iff line 55
  7. theorem OAI.SimplexChord.affine_exists_chord_iff line 66
  8. theorem OAI.SimplexChord.affine_maximal_chord line 87
  9. theorem OAI.SimplexChord.affine_intersection_homothety line 104
  10. theorem OAI.SimplexChord.linear_image_homothety line 165