English
A cycle has distinct interior vertices: for indices between 1 and length−1, the vertices p.getVert i are all distinct.
Русский
У цикла существуют различные внутренние вершины: индексы между 1 и length−1 соответствуют попарно различным вершинам p.getVert i.
LaTeX
$$p.IsCycle \Rightarrow (\forall i,j, 1 \le i,j \le p.length - 1 \Rightarrow p.getVert i \neq p.getVert j)$$
Lean4
theorem getVert_injOn' {p : G.Walk u u} (hpc : p.IsCycle) : Set.InjOn p.getVert {i | i ≤ p.length - 1} :=
by
intro n hn m hm hnm
simp only [Set.mem_setOf_eq] at *
have := hpc.three_le_length
have : p.length - n = p.length - m :=
Walk.length_reverse _ ▸
hpc.reverse.getVert_injOn (by simp only [Walk.length_reverse, Set.mem_setOf_eq]; cutsat)
(by simp only [Walk.length_reverse, Set.mem_setOf_eq]; cutsat)
(by
simp [Walk.getVert_reverse, show p.length - (p.length - n) = n by cutsat, hnm,
show p.length - (p.length - m) = m by cutsat])
cutsat
