equiv — Mathlib

English

There is an equivalence between elements of the HNN extension and words in normal form, implemented by mapping elements to their word and vice versa.

Русский

Существуют эквивалентности между элементами HNN-расширения и словами в нормальной форме: элемент ↔ слово и обратно.

LaTeX

$$$\\mathrm{equiv} : \\mathrm{HNNExtension}\\; G\\; A\\; B\\; \\varphi \\;\\simeq\\; \\mathrm{NormalWord}\\; d.$$$

Lean4

/-- The equivalence between elements of the HNN extension and words in normal form. -/
noncomputable def equiv : HNNExtension G A B φ ≃ NormalWord d :=
  { toFun := fun g => g • empty, invFun := fun w => w.prod φ, left_inv := fun g => by simp [prod_smul]
    right_inv := fun w => by simp }

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