reverse

Mathlib.Combinatorics.SimpleGraph.Paths

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

← MathLib Explorer

English

The reverse of a cycle is a cycle.

Русский

Обратный ход цикла является циклом.

LaTeX

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

Lean4

protected theorem reverse {p : G.Walk u u} (h : p.IsCycle) : p.reverse.IsCycle :=
  by
  simp only [Walk.isCycle_def, nodup_tail_support_reverse] at h ⊢
  exact ⟨h.1.reverse, fun h' ↦ h.2.1 (by simp_all [← Walk.length_eq_zero_iff]), h.2.2⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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