degree_induce_of_neighborSet_subset

English

If the neighbor set of v is contained in s, then the degree in the induced subgraph on s equals the degree in G.

Русский

Если множество соседей v содержится в s, то deg_(G|s)(v) = deg_G(v).

LaTeX

$$$ (G.induce s).degree v = G.degree v $$$

Lean4

/-- If the neighbor set of a vertex `v` is a subset of `s`, then the degree of the vertex in the
induced subgraph of `s` is the same as in `G`. -/
theorem degree_induce_of_neighborSet_subset {v : s} (h : G.neighborSet v ⊆ s) : (G.induce s).degree v = G.degree v := by
  simp_rw [← card_neighborFinset_eq_degree, ← map_neighborFinset_induce_of_neighborSet_subset h, card_map]

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