snd_ne_penultimate — Mathlib

English

For a cycle p, the vertices immediately around adjacent indices i−1, i+1 are distinct from p.getVert i.

Русский

Для цикла p вершина p.getVert i не равна соседним вершинам p.getVert i−1 и p.getVert i+1, и наоборот.

LaTeX

$$p.IsCycle \Rightarrow p.getVert(i-1) \neq p.getVert(i+1) \text{ for suitable } i$$

Lean4

theorem snd_ne_penultimate {p : G.Walk u u} (hp : p.IsCycle) : p.snd ≠ p.penultimate :=
  by
  intro h
  have := hp.three_le_length
  apply hp.getVert_injOn (by simp; cutsat) (by simp; cutsat)at h
  cutsat

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