labelledCopyCount — Mathlib

English

labelledCopyCount(G,H) counts the labelled copies of H in G, i.e., the number of graph embeddings from H to G.

Русский

labelledCopyCount(G,H) подсчитывает аннотированные копии H в G, т.е. число вложений графа H в G.

LaTeX

$$\mathrm{labelledCopyCount}(G,H) = |\mathrm{Copy}(H,G)|$$

Lean4

/-- `G.labelledCopyCount H` is the number of labelled copies of `H` in `G`, i.e. the number of graph
embeddings from `H` to `G`. See `SimpleGraph.copyCount` for the number of unlabelled copies. -/
noncomputable def labelledCopyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
  classical exact Fintype.card (Copy H G)

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