reverse_inj

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#Composition.reverse_inj

English

Two reverses are equal if and only if the originals are equal.

Русский

Две развёртки равны тогда и только тогда, когда исходные композиции равны.

LaTeX

$$$\\forall c_1,c_2,\\ c_1.\\mathrm{reverse} = c_2.\\mathrm{reverse} \\iff c_1=c_2.$$$

Lean4

@[simp]
theorem reverse_inj {c₁ c₂ : Composition n} : c₁.reverse = c₂.reverse ↔ c₁ = c₂ :=
  reverse_injective.eq_iff

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

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

Разделы

Аффилиация

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