copyCount_of_isEmpty — Mathlib

English

labelledCopyCount(G,H) counts labelled copies; in particular, it equals the cardinality of Copy(H,G).

Русский

labelledCopyCount(G,H) считает аннотированные копии; в частности, равно кардинальности Copy(H,G).

LaTeX

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

Lean4

@[simp]
theorem copyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) : G.copyCount H = 1 :=
  by
  cases nonempty_fintype W
  exact
    (copyCount_le_labelledCopyCount.trans_eq <| labelledCopyCount_of_isEmpty ..).antisymm <|
      copyCount_pos.2 <| .of_isEmpty

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