Bridge from finite graph densities to Mathlib's copy count

The finite-density development originally counted injective homomorphisms directly as filtered vertex maps. Mathlib's public numerator is SimpleGraph.labelledCopyCount, the cardinality of the bundled SimpleGraph.Copy type. This file proves the two counts identical and records Mathlib's host-first argument order.

theorem SimpleGraph.card_filter_injective_le_comap_eq_labelledCopyCount {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph W) (H : SimpleGraph V) : {f : W → V | Function.Injective f ∧ F ≤ SimpleGraph.comap f H}.card = H.labelledCopyCount F

Mathlib's labeled-copy count is the filtered count of injective vertex maps that preserve adjacency. The theorem is generic so that no concrete type's decidability instance competes with the classical instance hidden inside labelledCopyCount.

theorem SimpleGraph.injHomCount_eq_labelledCopyCount {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.injHomCount H = H.labelledCopyCount F

The project's injective-homomorphism numerator is Mathlib's labeled-copy count, with Mathlib's host-first argument order.