English
The product of two Kleene algebras α × β is a Kleene algebra, with operations defined componentwise: (a,b)^* = (a^*, b^*), etc.
Русский
Произведение двух Kleene алгебр α × β является Kleene алгеброй; операции определяются по компонентам: (a,b)^* = (a^*, b^*), и т.д.
LaTeX
$$$\text{KleeneAlgebra}(\alpha \times \beta)$$$
Lean4
instance : KleeneAlgebra (α × β) :=
{ Prod.instIdemSemiring with
kstar := fun a ↦ (a.1∗, a.2∗)
one_le_kstar := fun _ ↦ ⟨one_le_kstar, one_le_kstar⟩
mul_kstar_le_kstar := fun _ ↦ ⟨mul_kstar_le_kstar, mul_kstar_le_kstar⟩
kstar_mul_le_kstar := fun _ ↦ ⟨kstar_mul_le_kstar, kstar_mul_le_kstar⟩
mul_kstar_le_self := fun _ _ ↦ And.imp mul_kstar_le_self mul_kstar_le_self
kstar_mul_le_self := fun _ _ ↦ And.imp kstar_mul_le_self kstar_mul_le_self }
