mk_eq_mk — Mathlib

English

For words w1, w2 in FreeMonoid(M ⊕ N), mk w1 = mk w2 if and only if w1 and w2 are related by the coproduct congruence coprodCon M N.

Русский

Для слов w1, w2 из FreeMonoid(M ⊕ N) выполнено: mk w1 = mk w2 тогда и только тогда, когда w1 и w2 связаны конгруэнцией копродукта coprodCon M N.

LaTeX

$$$ mk w_1 = mk w_2 \iff coprodCon\ M\ N\ w_1\ w_2 $$$

Lean4

@[to_additive]
theorem mk_eq_mk {w₁ w₂ : FreeMonoid (M ⊕ N)} : mk w₁ = mk w₂ ↔ coprodCon M N w₁ w₂ :=
  Con.eq _

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