cycleGraph_EulerianCircuit — Mathlib

English

There exists an Eulerian circuit in cycleGraph(n+3); i.e., a closed walk that traverses every edge exactly once.

Русский

Существет эйлеров цикл в cycleGraph(n+3); т. е. замкнутая прогулка, проходящая по каждому ребру ровно один раз.

LaTeX

$$$ cycleGraph\_EulerianCircuit(n) : (cycleGraph(n + 3)).Walk 0 0 $$$

Lean4

/-- Eulerian trail of `cycleGraph (n + 3)` -/
def cycleGraph_EulerianCircuit (n : ℕ) : (cycleGraph (n + 3)).Walk 0 0 :=
  have hadj : (cycleGraph (n + 3)).Adj 0 (Fin.last (n + 2)) := by simp [cycleGraph_adj]
  Walk.cons hadj (cycleGraph_EulerianCircuit_cons n (Fin.last (n + 2)))

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