other_adj_of_adj — Mathlib

English

In a cycle, from a directed edge v—w there exists another vertex w′ with v adjacent to w′ and w′ ≠ w.

Русский

В графе, содержащем цикл, из ребра v—w следует существует другой сосед w′ у v, отличный от w.

LaTeX

$$∃ w' (w' ≠ w ∧ G.Adj(v,w'))$$

Lean4

/-- Given a vertex with one edge in a graph of cycles this gives the other edge incident
to the same vertex.
-/
theorem other_adj_of_adj (h : G.IsCycles) (hadj : G.Adj v w) : ∃ w', w ≠ w' ∧ G.Adj v w' :=
  by
  simp_rw [← SimpleGraph.mem_neighborSet] at hadj ⊢
  have := h ⟨w, hadj⟩
  obtain ⟨w', hww'⟩ := (G.neighborSet v).exists_ne_of_one_lt_ncard (by cutsat) w
  exact ⟨w', ⟨hww'.2.symm, hww'.1⟩⟩

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