three_le_length — Mathlib

English

Let G be a simple graph and p a closed walk from a vertex v to itself. If p is a cycle, then its length is at least 3.

Русский

Пусть G — простой граф, а p — замкнутый ход from вершины v в саму себя. Если p является циклом, то длина p не меньше 3.

LaTeX

$$$p.IsCycle \Rightarrow 3 \le p.length$$$

Lean4

theorem three_le_length {v : V} {p : G.Walk v v} (hp : p.IsCycle) : 3 ≤ p.length :=
  by
  have ⟨⟨hp, hp'⟩, _⟩ := hp
  match p with
  | .nil => simp at hp'
  | .cons h .nil => simp at h
  | .cons _ (.cons _ .nil) => simp at hp
  | .cons _ (.cons _ (.cons _ _)) => simp_rw [SimpleGraph.Walk.length_cons]; cutsat

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