churchRosser — Mathlib

English

Re-statement of the word of a product: toWord (x*y) = reduce (toWord x ++ toWord y).

Русский

Повторное утверждение слова произведения: toWord(x*y) = reduce(toWord x ++ toWord y).

LaTeX

$$$\forall x,y : FreeGroup\,\alpha ,\; toWord (x * y) = \mathrm{reduce}(toWord x ++ toWord y)$$$

Lean4

/-- **Constructive Church-Rosser theorem** (compare `FreeGroup.Red.church_rosser`). -/
@[to_additive /-- **Constructive Church-Rosser theorem** (compare `FreeAddGroup.Red.church_rosser`). -/
    ]
def churchRosser (H12 : Red L₁ L₂) (H13 : Red L₁ L₃) : { L₄ // Red L₂ L₄ ∧ Red L₃ L₄ } :=
  ⟨reduce L₁, reduce.rev H12, reduce.rev H13⟩

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