NeWord — Mathlib

English

There is an equivalence between CoprodI M and Word M.

Русский

Существует эквивалентность между CoprodI M и Word M.

LaTeX

$$$$ \\mathrm{CoprodI} M \\cong \\mathrm{Word} M $$$$

Lean4

/-- A `NeWord M i j` is a representation of a non-empty reduced words where the first letter comes
from `M i` and the last letter comes from `M j`. It can be constructed from singletons and via
concatenation, and thus provides a useful induction principle. -/
inductive NeWord : ι → ι → Type _
  | singleton : ∀ {i : ι} (x : M i), x ≠ 1 → NeWord i i
  | append : ∀ {i j k l} (_w₁ : NeWord i j) (_hne : j ≠ k) (_w₂ : NeWord k l), NeWord i l

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