kstar_def — Mathlib

English

Let α and β be Kleene algebras. In the product α × β, the Kleene star is taken componentwise, i.e. for any a = (a1, a2) ∈ α × β, a* = (a1*, a2*).

Русский

Пусть α и β — алгебры Клинея. В произведении α × β операция звёздочки действует по компонентам: для любой пары a = (a1, a2) ∈ α × β верно a* = (a1*, a2*).

LaTeX

$$$ (a_1, a_2)^* = (a_1^*, a_2^*) $$$

Lean4

theorem kstar_def (a : α × β) : a∗ = (a.1∗, a.2∗) :=
  rfl

Похожие утверждения