isCycle_def — Mathlib

English

An isCycle p for a walk p from u to u is equivalent to p.IsTrail and p ≠ nil and p.support.tail.Nodup.

Русский

Цикл обхода p равен тому, что p является следом (IsTrail), p не пустой и хвост поддержки p без повторов.

LaTeX

$$isCycle_def : ∀ {u} (p : G.Walk u u), p.IsCycle ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup$$

Lean4

theorem isCycle_def {u : V} (p : G.Walk u u) : p.IsCycle ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup :=
  Iff.intro (fun h => ⟨h.1.1, h.1.2, h.2⟩) fun h => ⟨⟨h.1, h.2.1⟩, h.2.2⟩

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