isPath_reverse_iff

Mathlib.Combinatorics.SimpleGraph.Paths

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

← MathLib Explorer

English

A walk is a path iff its reverse is a path.

Русский

Ход является путём тогда и только тогда, когда его обратный ход является путём.

LaTeX

$$$ p.reverse.IsPath \iff p.IsPath $$$

Lean4

@[simp]
theorem isPath_reverse_iff {u v : V} (p : G.Walk u v) : p.reverse.IsPath ↔ p.IsPath := by
  constructor <;> intro h <;> convert h.reverse; simp

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

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

Разделы

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

Аффилиация

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