English
In axis-aligned setting, the parallelepiped spanned by coordinate-wise scalars forms a cuboid: its shape is a box determined by the bounds [0, a_i].
Русский
В ось-сконфигурации параллелепипед, образованный координатно-совпадающими скалярами, является кубоидом: коробка с пределами [0, a_i].
LaTeX
$$$\\mathrm{parallelepiped}(\\,\\{ a_i \\}_i) = \\mathrm{uIcc}(0, a)$, где $a=(a_i)_i$.$$
Lean4
/-- The axis aligned parallelepiped over `ι → ℝ` is a cuboid. -/
theorem parallelepiped_single [DecidableEq ι] (a : ι → ℝ) :
(parallelepiped fun i => Pi.single i (a i)) = Set.uIcc 0 a :=
by
ext x
simp_rw [Set.uIcc, mem_parallelepiped_iff, Set.mem_Icc, Pi.le_def, ← forall_and, Pi.inf_apply, Pi.sup_apply, ←
Pi.single_smul', Pi.one_apply, Pi.zero_apply, ← Pi.smul_apply', Finset.univ_sum_single (_ : ι → ℝ)]
constructor
· rintro ⟨t, ht, rfl⟩ i
specialize ht i
simp_rw [smul_eq_mul, Pi.mul_apply]
rcases le_total (a i) 0 with hai | hai
· rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai]
exact ⟨le_mul_of_le_one_left hai ht.2, mul_nonpos_of_nonneg_of_nonpos ht.1 hai⟩
· rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai]
exact ⟨mul_nonneg ht.1 hai, mul_le_of_le_one_left hai ht.2⟩
· intro h
refine ⟨fun i => x i / a i, fun i => ?_, funext fun i => ?_⟩
· specialize h i
rcases le_total (a i) 0 with hai | hai
· rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai] at h
exact ⟨div_nonneg_of_nonpos h.2 hai, div_le_one_of_ge h.1 hai⟩
· rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai] at h
exact ⟨div_nonneg h.1 hai, div_le_one_of_le₀ h.2 hai⟩
· specialize h i
simp only [smul_eq_mul, Pi.mul_apply]
rcases eq_or_ne (a i) 0 with hai | hai
· rw [hai, inf_idem, sup_idem, ← le_antisymm_iff] at h
rw [hai, ← h, zero_div, zero_mul]
· rw [div_mul_cancel₀ _ hai]
