fst_kstar — Mathlib

English

In α × β with a Kleene algebra structure, the first projection of the star equals the star of the first component: (a1, a2)*.1 = a1*.

Русский

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

LaTeX

$$$ (a_1, a_2)^*{}_1 = a_1^* $$$

Lean4

@[simp]
theorem fst_kstar (a : α × β) : a∗.1 = a.1∗ :=
  rfl

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