prod_injective — Mathlib

English

The mapping from words to their reduced product in the HNN extension is injective, ensuring a unique representative for each product.

Русский

Отображение слов в редуцированное произведение в HNN-расширении инъективно, обеспечивая уникальный представитель для каждого произведения.

LaTeX

$$$\\text{prod\_injective} : (\\mathrm{NormalWord}\\; d) \\to \\mathrm{HNNExtension}\\; G\\; A\\; B\\; \\varphi \\; \\text{Injective}$$$

Lean4

theorem prod_injective : Injective (fun w => w.prod φ : NormalWord d → HNNExtension G A B φ) :=
  (equiv φ d).symm.injective

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