ncard_neighborSet_toSubgraph_internal_eq_two

English

Under the same hypotheses as the previous lemma, the neighbor set at an internal vertex has cardinality 2.

Русский

При тех же предположениях множество соседей внутри вершины имеет кардинал 2.

LaTeX

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

Lean4

theorem ncard_neighborSet_toSubgraph_internal_eq_two {u} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath) (h : i ≠ 0)
    (h' : i < p.length) : (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2 :=
  by
  rw [hp.neighborSet_toSubgraph_internal h h']
  have : p.getVert (i - 1) ≠ p.getVert (i + 1) := by
    intro h
    have := hp.getVert_injOn (by rw [Set.mem_setOf_eq]; cutsat) (by rw [Set.mem_setOf_eq]; cutsat) h
    omega
  simp_all

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