English
For an orthonormal basis in one dimension, the parallelepiped is either [0,1] or [-1,0].
Русский
Для ортономерного базиса в одной размерности параллелепипед равен либо [0,1], либо [-1,0].
LaTeX
$$$\\mathrm{parallelepiped}(b) = Icc(0,1)$ или $= Icc(-1,0)$ для одномерного ортоновного базиса.$$
Lean4
theorem parallelepiped_orthonormalBasis_one_dim (b : OrthonormalBasis ι ℝ ℝ) :
parallelepiped b = Icc 0 1 ∨ parallelepiped b = Icc (-1) 0 :=
by
have e : ι ≃ Fin 1 := by
apply Fintype.equivFinOfCardEq
simp only [← finrank_eq_card_basis b.toBasis, finrank_self]
have B : parallelepiped (b.reindex e) = parallelepiped b :=
by
convert parallelepiped_comp_equiv b e.symm
ext i
simp only [OrthonormalBasis.coe_reindex]
rw [← B]
let F : ℝ → Fin 1 → ℝ := fun t => fun _i => t
have A : Icc (0 : Fin 1 → ℝ) 1 = F '' Icc (0 : ℝ) 1 :=
by
apply Subset.antisymm
· intro x hx
refine ⟨x 0, ⟨hx.1 0, hx.2 0⟩, ?_⟩
ext j
simp only [F, Subsingleton.elim j 0]
· rintro x ⟨y, hy, rfl⟩
exact ⟨fun _j => hy.1, fun _j => hy.2⟩
rcases orthonormalBasis_one_dim (b.reindex e) with (H | H)
· left
simp_rw [parallelepiped, H, A, Algebra.id.smul_eq_mul, mul_one]
simp only [F, Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, ← image_comp, Function.comp_apply,
image_id']
· right
simp_rw [H, parallelepiped, Algebra.id.smul_eq_mul, A]
simp only [F, Finset.univ_unique, Fin.default_eq_zero, mul_neg, mul_one, Finset.sum_neg_distrib,
Finset.sum_singleton, ← image_comp, Function.comp, image_neg_eq_neg, neg_Icc, neg_zero]
