Theorems · Theorem · combinatorics

SimpleGraph.copyCount_eq_card_image_copyToSubgraph

∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V]
  [inst_1 : Fintype { f // Function.Injective ⇑f }] [inst_2 : DecidableEq G.Subgraph],
  G.copyCount H = (Finset.image SimpleGraph.Copy.toSubgraph Finset.univ).card

Defined in

Mathlib.Combinatorics.SimpleGraph.Copy

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeFintypeDecidableEq