degree_induce_of_support_subset — Mathlib

English

If G.support ⊆ s, then for any vertex v ∈ s, deg_{G|s}(v) = deg_G(v).

Русский

Если поддержка G лежит внутри s, то для любой вершины v ∈ s deg_{G|s}(v) = deg_G(v).

LaTeX

$$$\\forall v \\in s:\\; (G.induce s).degree v = G.degree v$$$

Lean4

/-- If the support of the simple graph `G` is a subset of the set `s`, then the degree of vertices
in the induced subgraph of `s` are the same as in `G`. -/
theorem degree_induce_of_support_subset (h : G.support ⊆ s) (v : s) : (G.induce s).degree v = G.degree v :=
  degree_induce_of_neighborSet_subset <| (G.neighborSet_subset_support v).trans h

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