copyCount_eq_card_image_copyToSubgraph

English

copyCount(G,H) equals the card image of a subgraph mapping, under certain injective constraints.

Русский

copyCount(G,H) равно мощности образа отображения подграфа при определённых предпосылках инъективности.

LaTeX

$$copyCount(G,H) = card( image SimpleGraph.Copy.toSubgraph Univ )$$

Lean4

theorem copyCount_eq_card_image_copyToSubgraph [Fintype { f : H →g G // Injective f }] [DecidableEq G.Subgraph] :
    copyCount G H = #((Finset.univ : Finset (H.Copy G)).image Copy.toSubgraph) :=
  by
  rw [copyCount]
  congr
  refine Finset.coe_injective ?_
  simpa [-Copy.range_toSubgraph] using Copy.range_toSubgraph.symm

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