parallelepiped_eq_sum_segment — Mathlib

English

A parallelepiped can be expressed as a sum of segments from 0 to v_i for each i.

Русский

Параллелепипед можно выразить как сумма отрезков от 0 до v_i для каждого i.

LaTeX

$$$\\mathrm{parallelepiped}(v) = \\sum_i \\mathrm{segment}(0, v_i).$$$

Lean4

theorem parallelepiped_eq_sum_segment (v : ι → E) : parallelepiped v = ∑ i, segment ℝ 0 (v i) :=
  by
  ext
  simp only [mem_parallelepiped_iff, Set.mem_finset_sum, Finset.mem_univ, forall_true_left, segment_eq_image, smul_zero,
    zero_add, ← Set.pi_univ_Icc, Set.mem_univ_pi]
  constructor
  · rintro ⟨t, ht, rfl⟩
    exact ⟨t • v, fun {i} => ⟨t i, ht _, by simp⟩, rfl⟩
  rintro ⟨g, hg, rfl⟩
  choose t ht hg using @hg
  refine ⟨@t, @ht, ?_⟩
  simp_rw [hg]

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