darts_injective

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

The map sending a walk to its list of darts is injective.

Русский

Отображение хода в список дуг инъективно.

LaTeX

$$$ \text{darts}: G.Walk\,u\,v \to \mathrm{List}(G.Dart) \; \text{ injective.}$$$

Lean4

theorem darts_injective {u v : V} : Function.Injective (Walk.darts : G.Walk u v → List G.Dart) :=
  edges_injective.of_comp

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

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

Разделы

Аффилиация

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