English
For a linear basis b, parallelepiped(b) equals the set of x with each coordinate in the basis lying in [0,1].
Русский
Для базиса b параллелепипед(b) — это множество x, для которого каждое координатное по базису лежит в [0,1].
LaTeX
$$$\\mathrm{parallelepiped}(b) = \\{ x : E : \\; \\forall i,\\; b^{-1}(x)_i \\in [0,1]\\}.$$$
Lean4
theorem parallelepiped_basis_eq (b : Basis ι ℝ E) : parallelepiped b = {x | ∀ i, b.repr x i ∈ Set.Icc 0 1} := by
classical
ext x
simp_rw [mem_parallelepiped_iff, mem_setOf_eq, b.ext_elem_iff, _root_.map_sum, map_smul, Finset.sum_apply',
Basis.repr_self, Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.single_apply, Finset.sum_ite_eq',
Finset.mem_univ, ite_true, mem_Icc, Pi.le_def, Pi.zero_apply, Pi.one_apply, ← forall_and]
aesop
