ncard_neighborSet_toSubgraph_eq_two

English

If p is a cycle, there exists a cycle with a specified second vertex corresponding to w and with the same vertex set as p’s subgraph.

Русский

Если p — цикл, существует цикл с заданной второй вершиной, сохраняющий множество вершин подграфа p.

LaTeX

$$$\exists p' : G.Walk v v, p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts$$$

Lean4

theorem ncard_neighborSet_toSubgraph_eq_two {u v} {p : G.Walk u u} (hpc : p.IsCycle) (h : v ∈ p.support) :
    (p.toSubgraph.neighborSet v).ncard = 2 :=
  by
  simp only [SimpleGraph.Walk.mem_support_iff_exists_getVert] at h ⊢
  obtain ⟨i, hi⟩ := h
  by_cases he : i = 0 ∨ i = p.length
  · have huv : u = v := by aesop
    rw [← huv, hpc.neighborSet_toSubgraph_endpoint]
    exact Set.ncard_pair hpc.snd_ne_penultimate
  push_neg at he
  rw [← hi.1, hpc.neighborSet_toSubgraph_internal he.1 (by cutsat)]
  exact Set.ncard_pair (hpc.getVert_sub_one_ne_getVert_add_one (by cutsat))

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