getVert_sub_one_ne_getVert_add_one

English

For a cycle p, the same interior injectivity properties hold as in previous lemmas; endpoints are excluded.

Русский

Для цикла p границы исключаются из рассмотрения инъективности вершин; внутренние индексы остаются различными.

LaTeX

$$p.IsCycle \Rightarrow (additional boundary injectivity statements)$$

Lean4

theorem getVert_sub_one_ne_getVert_add_one {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle) (h : i ≤ p.length) :
    p.getVert (i - 1) ≠ p.getVert (i + 1) := by
  intro h'
  have hl := hpc.three_le_length
  by_cases hi' : i ≥ p.length - 1
  · rw [p.getVert_of_length_le (by cutsat : p.length ≤ i + 1), hpc.getVert_endpoint_iff (by cutsat)] at h'
    cutsat
  have :=
    hpc.getVert_injOn' (by simp only [Set.mem_setOf_eq, Nat.sub_le_iff_le_add]; cutsat)
      (by simp only [Set.mem_setOf_eq]; cutsat) h'
  cutsat

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