le_card_edgeFinset_killCopies_add_copyCount

English

The total number of edges in G is at most the edges in G.killCopies(H) plus the number of copies of G in H.

Русский

Общее число рёбер G не больше числа рёбер G.killCopies(H) плюс число копий G в H.

LaTeX

$$$ |E(G)| \le |E(G.killCopies(H))| + copyCount_G(H) $$$

Lean4

/-- Removing an edge from `H` for each subgraph isomorphic to `G` means that the number of edges
we've removed is at most the number of copies of `G` in `H`. -/
theorem le_card_edgeFinset_killCopies_add_copyCount [Fintype V] :
    #G.edgeFinset ≤ #(G.killCopies H).edgeFinset + G.copyCount H :=
  tsub_le_iff_right.1 le_card_edgeFinset_killCopies

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