copyCount — Mathlib

English

copyCount(G,H) equals the cardinality of the image of Copy.toSubgraph from univ over the copies.

Русский

copyCount(G,H) равно мощности образа Copy.toSubgraph от множества копий.

LaTeX

$$\mathrm{copyCount}(G,H) = \#\big((\mathrm{Finset.univ} : \mathrm{Finset}) (H.G\{G\}).image Copy.toSubgraph\big)$$

Lean4

/-- `G.copyCount H` is the number of unlabelled copies of `H` in `G`, i.e. the number of subgraphs
of `G` isomorphic to `H`. See `SimpleGraph.labelledCopyCount` for the number of labelled copies. -/
noncomputable def copyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
  classical exact #{G' : G.Subgraph | Nonempty (H ≃g G'.coe)}

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