finite_neighborSet_toSubgraph — Mathlib

English

In the subgraph induced by a walk, the neighbor set of any vertex is finite.

Русский

Во подграфе, индуцируемом обходом, множество соседей любой вершины конечно.

LaTeX

$$$ (p.toSubgraph.neighborSet w).Finite $$$

Lean4

@[simp]
theorem finite_neighborSet_toSubgraph (p : G.Walk u v) : (p.toSubgraph.neighborSet w).Finite := by
  induction p with
  | nil =>
    rw [Walk.toSubgraph, neighborSet_singletonSubgraph]
    apply Set.toFinite
  | cons ha _ ih =>
    rw [Walk.toSubgraph, Subgraph.neighborSet_sup]
    refine Set.Finite.union ?_ ih
    refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)
    apply Set.toFinite

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