labelledCopyCount_of_isEmpty — Mathlib

English

If W is empty, then the labelled copy count is 1 for any G and H.

Русский

Если W пусто, то для любого G и H число аннотированных копий равно 1.

LaTeX

$$[IsEmpty W] ⇒ \mathrm{labelledCopyCount}(G,H) = 1$$

Lean4

@[simp]
theorem labelledCopyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) : G.labelledCopyCount H = 1 :=
  by
  convert Fintype.card_unique
  exact { default := ⟨default, isEmptyElim⟩, uniq := fun _ ↦ Subsingleton.elim _ _ }

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