mem_parallelepiped_iff — Mathlib

English

A point x lies in parallelepiped(v) iff there exists a vector t with coordinates in [0,1] such that x = ∑ t_i v_i.

Русский

Точка x принадлежит параллелепипеду(v), тогда существует вектор t с координатами в [0,1], что x = ∑ t_i v_i.

LaTeX

$$$x \\in \\mathrm{parallelepiped}(v) \\iff \\exists t \\in \\mathrm{Icc}(0,1)^{\\!\\,\\,ι}, \\, x = \\sum_i t_i v_i.$$$

Lean4

theorem mem_parallelepiped_iff (v : ι → E) (x : E) :
    x ∈ parallelepiped v ↔ ∃ t ∈ Icc (0 : ι → ℝ) 1, x = ∑ i, t i • v i := by simp [parallelepiped, eq_comm]

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