Counting ordered pairs of distinct agents by species

For a configuration c : Fin n → S, the ordered pairs (u, v) of distinct agents whose species form the unordered pair {A, B} are 2·#A·#B if A ≠ B and #A·(#A - 1) if A = B, where #A is the number of agents of species A; there are n·(n - 1) ordered pairs of distinct agents. This is the counting behind the key identity of CRN-1.

theorem Crn.card_filter_pairs {S : Type u_1} [DecidableEq S] {n : ℕ} (c : Fin n → S) (z : Sym2 S) : {p : { p : Fin n × Fin n // p.1 ≠ p.2 } | s(c (↑p).1, c (↑p).2) = z}.card = {p ∈ Finset.univ.offDiag | s(c p.1, c p.2) = z}.card

Filtering ordered pairs of distinct agents is filtering the off-diagonal of Fin n × Fin n.

theorem Crn.card_pairs {n : ℕ} : Fintype.card { p : Fin n × Fin n // p.1 ≠ p.2 } = n * (n - 1)

There are n·(n - 1) ordered pairs of distinct agents.

theorem Crn.card_pairs_of_ne {S : Type u_1} [DecidableEq S] {n : ℕ} (c : Fin n → S) {A B : S} (hAB : A ≠ B) : {p ∈ Finset.univ.offDiag | s(c p.1, c p.2) = s(A, B)}.card = 2 * {v : Fin n | c v = A}.card * {v : Fin n | c v = B}.card

Ordered pairs of distinct agents with species {A, B}, A ≠ B: 2·#A·#B.

theorem Crn.card_pairs_of_eq {S : Type u_1} [DecidableEq S] {n : ℕ} (c : Fin n → S) (A : S) : {p ∈ Finset.univ.offDiag | s(c p.1, c p.2) = s(A, A)}.card = {v : Fin n | c v = A}.card * ({v : Fin n | c v = A}.card - 1)

Ordered pairs of distinct agents with species {A, A}: #A·(#A - 1).