getVert_endpoint_iff — Mathlib

English

For a cycle p and i ≤ length, p.getVert i equals the starting vertex u if and only if i = 0 or i = length.

Русский

Для цикла p вершина p.getVert i равна начальной вершине u тогда и только тогда, когда i = 0 или i = length.

LaTeX

$$p.IsCycle \Rightarrow i \le p.length \Rightarrow (p.getVert i = u \iff i = 0 \lor i = p.length)$$

Lean4

theorem getVert_endpoint_iff {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle) (hl : i ≤ p.length) :
    p.getVert i = u ↔ i = 0 ∨ i = p.length := by
  refine ⟨?_, by aesop⟩
  rw [or_iff_not_imp_left]
  intro h hi
  exact
    hpc.getVert_injOn (by simp only [Set.mem_setOf_eq]; cutsat) (by simp only [Set.mem_setOf_eq]; cutsat)
      (h.symm ▸ (Walk.getVert_length p).symm)

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