snd_of_toSubgraph_adj — Mathlib

English

A variant of the internal neighbor-count result, confirming two neighbors for the internal vertex under the same conditions as before.

Русский

Вариант предыдущего факта о соседях внутри — два соседа при тех же условиях.

LaTeX

$$$ (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2 $$$

Lean4

theorem snd_of_toSubgraph_adj {u v v'} {p : G.Walk u v} (hp : p.IsPath) (hadj : p.toSubgraph.Adj u v') : p.snd = v' :=
  by
  have ⟨i, hi⟩ := p.toSubgraph_adj_iff.mp hadj
  simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at hi
  rcases hi.1 with ⟨hl1, rfl⟩ | ⟨hr1, hr2⟩
  · have : i = 0 :=
      by
      apply hp.getVert_injOn (by rw [Set.mem_setOf]; cutsat) (by rw [Set.mem_setOf]; cutsat)
      rw [p.getVert_zero, hl1]
    simp [this]
  · have : i + 1 = 0 :=
      by
      apply hp.getVert_injOn (by rw [Set.mem_setOf]; cutsat) (by rw [Set.mem_setOf]; cutsat)
      rw [p.getVert_zero, hr2]
    contradiction

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