invRev_injective

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.invRev_injective

English

InvRev is injective: if invRev(L1) = invRev(L2) then L1 = L2.

Русский

InvRev инъективна: если invRev(L1) = invRev(L2), то L1 = L2.

LaTeX

$$$\forall L_1,L_2:\, \mathrm{invRev}(L_1) = \mathrm{invRev}(L_2) \Rightarrow L_1 = L_2.$$$

Lean4

@[to_additive]
theorem invRev_injective : Function.Injective (@invRev α) :=
  invRev_involutive.injective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru