rotate_edges

Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp

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

English

Rotation preserves the edge sequence up to rotation: (rotate_edges c h).edges ~r c.edges.

Русский

Поворот сохраняет последовательность рёбер вплоть до вращения: (rotate_edges c h).edges ~r c.edges.

LaTeX

$$$ (rotate_edges c h).edges ~r c.edges $$$

Lean4

theorem rotate_edges {u v : V} (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).edges ~r c.edges :=
  (rotate_darts c h).map _

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

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

Разделы

Аффилиация

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