English
If x=(x1,x2), y=(y1,y2), z=(z1,z2) in M × N satisfy semiconjugacy in each coordinate, then the pair is semiconjugate in the product: x y z in M × N.
Русский
Пусть x=(x1,x2), y=(y1,y2), z=(z1,z2) в M × N удовлетворяют полному свойству полусопряжения по каждой координате; тогда в произведении выполняется semiconjugacy.
LaTeX
$$$\text{SemiconjBy}(x_1,y_1,z_1) \wedge \text{SemiconjBy}(x_2,y_2,z_2) \Rightarrow \text{SemiconjBy}((x_1,x_2),(y_1,y_2),(z_1,z_2))$$$
Lean4
@[to_additive AddSemiconjBy.prod]
theorem prod {x y z : M × N} (hm : SemiconjBy x.1 y.1 z.1) (hn : SemiconjBy x.2 y.2 z.2) : SemiconjBy x y z :=
Prod.ext hm hn
