English
The parallelepiped of a cartesian product of two bases equals the product of their parallelepipeds.
Русский
Параллелепипед произведения двух базисов равен произведению их параллелепипедов.
LaTeX
$$$ (v.pos w).parallelepiped = v.parallelepiped.prod w.parallelepiped $.$$
Lean4
theorem prod_parallelepiped (v : Basis ι ℝ E) (w : Basis ι' ℝ F) :
(v.prod w).parallelepiped = v.parallelepiped.prod w.parallelepiped :=
by
ext x
simp only [Basis.coe_parallelepiped, TopologicalSpace.PositiveCompacts.coe_prod, Set.mem_prod, mem_parallelepiped_iff]
constructor
· intro h
rcases h with ⟨t, ht1, ht2⟩
constructor
· use t ∘ Sum.inl
constructor
· exact ⟨(ht1.1 <| Sum.inl ·), (ht1.2 <| Sum.inl ·)⟩
simp [ht2, Prod.fst_sum]
· use t ∘ Sum.inr
constructor
· exact ⟨(ht1.1 <| Sum.inr ·), (ht1.2 <| Sum.inr ·)⟩
simp [ht2, Prod.snd_sum]
intro h
rcases h with ⟨⟨t, ht1, ht2⟩, ⟨s, hs1, hs2⟩⟩
use Sum.elim t s
constructor
· constructor
· change ∀ x : ι ⊕ ι', 0 ≤ Sum.elim t s x
aesop
· change ∀ x : ι ⊕ ι', Sum.elim t s x ≤ 1
aesop
ext
· simp [ht2, Prod.fst_sum]
· simp [hs2, Prod.snd_sum]
