parallelepiped_eq_convexHull — Mathlib

English

A parallelepiped is the convex hull of its vertices, i.e., the vertices are 0 and v_i for all i.

Русский

Параллелепипед является выпуклой оболочкой своих вершин, т.е. вершин: 0 и v_i для всех i.

LaTeX

$$$\\mathrm{parallelepiped}(v) = \\operatorname{convexHull}(\\{ 0, v_i : i\\})$.$$

Lean4

/-- A `parallelepiped` is the convex hull of its vertices -/
theorem parallelepiped_eq_convexHull (v : ι → E) : parallelepiped v = convexHull ℝ (∑ i, {(0 : E), v i}) := by
  simp_rw [convexHull_sum, convexHull_pair, parallelepiped_eq_sum_segment]

Похожие утверждения