injective — Mathlib

English

Let b be a free group basis of G over ι. Then the associated generating map i ↦ b(i) is injective; i.e., b(i) = b(j) implies i = j.

Русский

Пусть b является базисом свободной группы G над ι. Тогда отображение i ↦ b(i) инъективно; то есть b(i) = b(j) вызывает i = j.

LaTeX

$$$\forall i,j \in ι\,,\; b(i)=b(j) \Rightarrow i=j$$$

Lean4

protected theorem injective (b : FreeGroupBasis ι G) : Injective b :=
  b.repr.symm.injective.comp FreeGroup.of_injective

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