card_edgeFinset_induce_support — Mathlib

English

Equality of edge counts holds when restricting to the support: the induced subgraph on G.support has the same number of edges as G.

Русский

Для подмножества поддержки графа число рёбер совпадает с числом рёбер графа: индуцированный подграф на G.support имеет то же число рёбер, что и G.

LaTeX

$$$#(G.induce G.support).edgeFinset = #G.edgeFinset$$$

Lean4

theorem card_edgeFinset_induce_support : #(G.induce G.support).edgeFinset = #G.edgeFinset :=
  card_edgeFinset_induce_of_support_subset subset_rfl

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