English
The coordinates of the product basis are given by a simple piecewise rule: the i-th basis vector of v.prod w is either the i-th vector from v (when i is from the left copy) or the i-th vector from w (when i is from the right copy).
Русский
Координаты произведённого базиса заданы по простому правилу: вектор i-й размерности из v.prod w берётся либо из v, либо из w в зависимости от того, принадлежит ли индекс левой или правой копии.
LaTeX
$$$\forall i:\; (v.prod w)_i = \begin{cases} v_i & \text{if } i \in ι_1\;, \\ w_j & \text{if } i \in ι_2\; \end{cases}$$$
Lean4
@[simp]
theorem prod_apply (v : OrthonormalBasis ι₁ 𝕜 E) (w : OrthonormalBasis ι₂ 𝕜 F) :
∀ i : ι₁ ⊕ ι₂, v.prod w i = Sum.elim ((LinearMap.inl 𝕜 E F) ∘ v) ((LinearMap.inr 𝕜 E F) ∘ w) i :=
by
rw [Sum.forall]
unfold OrthonormalBasis.prod
aesop
