English
Let a1, a2, a3 be families indexed by i with a semiconjugacy a1 ≺ a2 ≺ a3 componentwise. Then their PiTensorProduct tensor expressions satisfy the same semiconjugacy relation: tprod R a1 semiconj to tprod R a2 via tprod R a3.
Русский
Пусть {a_i}^ι_{i} — семейство элементов, удовлетворяющее компонентно полуопряжённости a1 к a2 через a3. Тогда их произведение по тензору сохраняет это полуопряжение: tprod R a1 полусопряжено к tprod R a2 через tprod R a3.
LaTeX
$$$SemiconjBy\\ (tprod\\ R\\ a_1)\\ (tprod\\ R\\ a_2)\\ (tprod\\ R\\ a_3)$$$
Lean4
theorem _root_.SemiconjBy.tprod {a₁ a₂ a₃ : Π i, A i} (ha : SemiconjBy a₁ a₂ a₃) :
SemiconjBy (tprod R a₁) (tprod R a₂) (tprod R a₃) := by rw [SemiconjBy, tprod_mul_tprod, tprod_mul_tprod, ha]
