reverse_bijective

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

The reverse map on walks is bijective: it is both injective and surjective.

Русский

Обратное отображение на путях биективно: оно и инъективно, и сюръективно.

LaTeX

$$$$\forall {u,v},\text{ reverse is bijective on } G.Walk u v,$$$$

Lean4

theorem reverse_bijective {u v : V} : Function.Bijective (reverse : G.Walk u v → _) :=
  And.intro reverse_injective reverse_surjective

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

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

Разделы

Аффилиация

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