neighborSet_toSubgraph_startpoint

English

For a path p, the neighbor set of the start vertex is the singleton { its second vertex }.

Русский

Для пути соседи начальной вершины образуют множество из одной вершины — следующей за ней.

LaTeX

$$$ p.IsPath \Rightarrow p.toSubgraph.neighborSet p.start = \{ p.snd \} $$$

Lean4

theorem neighborSet_toSubgraph_startpoint {u v} {p : G.Walk u v} (hp : p.IsPath) (hnp : ¬p.Nil) :
    p.toSubgraph.neighborSet u = { p.snd } :=
  by
  have hadj1 := p.toSubgraph_adj_snd hnp
  ext v
  simp_all only [Subgraph.mem_neighborSet, Set.mem_singleton_iff, SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq,
    Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
  refine ⟨?_, by simp_all⟩
  rintro ⟨i, hl | hr⟩
  · have : i = 0 :=
      by
      apply hp.getVert_injOn (by rw [Set.mem_setOf]; cutsat) (by rw [Set.mem_setOf]; cutsat)
      simp_all
    simp_all
  · have : i + 1 = 0 :=
      by
      apply hp.getVert_injOn (by rw [Set.mem_setOf]; cutsat) (by rw [Set.mem_setOf]; cutsat)
      simp_all
    contradiction

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