reverse_isTrail_iff

Mathlib.Combinatorics.SimpleGraph.Paths

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$ p.\mathrm{reverse}.IsTrail \iff p.IsTrail $$$

Lean4

@[simp]
theorem reverse_isTrail_iff {u v : V} (p : G.Walk u v) : p.reverse.IsTrail ↔ p.IsTrail := by
  constructor <;>
    · intro h
      convert h.reverse _
      try rw [reverse_reverse]

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

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

Разделы

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

Аффилиация

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