card_edgeFinset_induce_of_support_subset

English

If G.support ⊆ s, then the number of edges in the induced subgraph on s equals the number of edges in G.

Русский

Если поддержка G лежит внутри s, то число рёбер индуцированного подграфа на s равно числу рёбер графа G.

LaTeX

$$$\\#(G.induce s).edgeFinset = \\#G.edgeFinset$$$

Lean4

/-- If the support of the simple graph `G` is a subset of the set `s`, then the induced subgraph of
`s` has the same number of edges as `G`. -/
theorem card_edgeFinset_induce_of_support_subset (h : G.support ⊆ s) : #(G.induce s).edgeFinset = #G.edgeFinset := by
  rw [← map_edgeFinset_induce_of_support_subset h, card_map]

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