English
Under a linear map f, the image of parallelepiped(v) equals parallelepiped(f ∘ v).
Русский
Образ параллелепипеда(v) под линейным отображением f равен параллелепипеду(f ∘ v).
LaTeX
$$$f''\\mathrm{parallelepiped}(v) = \\mathrm{parallelepiped}(f \\circ v).$$$
Lean4
/-- Reindexing a family of vectors does not change their parallelepiped. -/
@[simp]
theorem parallelepiped_comp_equiv (v : ι → E) (e : ι' ≃ ι) : parallelepiped (v ∘ e) = parallelepiped v :=
by
simp only [parallelepiped]
let K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a : ι' => ℝ) e
have : Icc (0 : ι → ℝ) 1 = K '' Icc (0 : ι' → ℝ) 1 :=
by
rw [← Equiv.preimage_eq_iff_eq_image]
ext x
simp only [K, mem_preimage, mem_Icc, Pi.le_def, Pi.zero_apply, Equiv.piCongrLeft'_apply, Pi.one_apply]
refine ⟨fun h => ⟨fun i => ?_, fun i => ?_⟩, fun h => ⟨fun i => h.1 (e.symm i), fun i => h.2 (e.symm i)⟩⟩
· simpa only [Equiv.symm_apply_apply] using h.1 (e i)
· simpa only [Equiv.symm_apply_apply] using h.2 (e i)
rw [this, ← image_comp]
ext x
have := fun z : ι' → ℝ => e.symm.sum_comp fun i => z i • v (e i)
simp_rw [Equiv.apply_symm_apply] at this
simp_rw [Function.comp_apply, mem_image, mem_Icc, K, Equiv.piCongrLeft'_apply, this]
-- The parallelepiped associated to an orthonormal basis of `ℝ` is either `[0, 1]` or `[-1, 0]`.
