reverse_injective

Mathlib.Combinatorics.SimpleGraph.Walk

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.reverse_injective

English

The reverse map on walks is injective: if reverse(p) = reverse(q) then p = q.

Русский

Обратное отображение на путях инъективно: если reverse(p) = reverse(q), то p = q.

LaTeX

$$$$\forall p,q:\, G.Walk,\ \text{reverse}(p) = \text{reverse}(q) \Rightarrow p = q.$$$$

Lean4

theorem reverse_injective {u v : V} : Function.Injective (reverse : G.Walk u v → _) :=
  RightInverse.injective reverse_reverse

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

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

Разделы

Аффилиация

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