existsUnique_ne_adj — Mathlib

English

In a cycle graph, from a vertex v with neighbor w there is a unique neighbor w′ ≠ w such that v is adjacent to w′.

Русский

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

LaTeX

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

Lean4

theorem existsUnique_ne_adj (h : G.IsCycles) (hadj : G.Adj v w) : ∃! w', w ≠ w' ∧ G.Adj v w' :=
  by
  obtain ⟨w', ⟨hww, hww'⟩⟩ := h.other_adj_of_adj hadj
  use w'
  refine ⟨⟨hww, hww'⟩, ?_⟩
  intro y ⟨hwy, hwy'⟩
  obtain ⟨x, y', hxy'⟩ := Set.ncard_eq_two.mp (h ⟨w, hadj⟩)
  simp_rw [← SimpleGraph.mem_neighborSet] at *
  aesop

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