isCycle_reverse

Mathlib.Combinatorics.SimpleGraph.Paths

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

English

The reverse of a cycle remains a cycle.

Русский

Обратный цикл остаётся циклом.

LaTeX

$$p.reverse.IsCycle \Leftrightarrow p.IsCycle$$

Lean4

@[simp]
theorem isCycle_reverse {p : G.Walk u u} : p.reverse.IsCycle ↔ p.IsCycle
    where
  mp h := by simpa using h.reverse
  mpr := .reverse

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

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

Разделы

Аффилиация

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