reverse_injective

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.reverse_injective

English

The reverse operation is injective: if reverse s = reverse t, then s = t.

Русский

Операция разворота инъективна: если reverse s = reverse t, то s = t.

LaTeX

$$$$\\forall s,t:\\\\mathrm{List}\\\\alpha,\\\\ \\mathrm{reverse}(s) = \\\\mathrm{reverse}(t) \\\\Rightarrow s = t.$$$$

Lean4

@[simp]
theorem reverse_injective : Injective (@reverse α) :=
  reverse_involutive.injective

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

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

Разделы

Аффилиация

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