parallelepiped — Mathlib

English

The parallelepiped spanned by a finite family of vectors is the image of the unit cube under the linear map t ↦ ∑ t_i v_i, where t ∈ Icc(0,1).

Русский

Параллелепипед, образованный конечной семейством векторов, есть образ единичного куба при линейном отображении t ↦ ∑ t_i v_i, где t ∈ Icc(0,1).

LaTeX

$$$\\mathrm{parallelepiped}(v) = \\{ \\sum_i t_i v_i : t_i \\in [0,1] \\}.$$$

Lean4

/-- The closed parallelepiped spanned by a finite family of vectors. -/
def parallelepiped (v : ι → E) : Set E :=
  (fun t : ι → ℝ => ∑ i, t i • v i) '' Icc 0 1

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