English
The image of the off-diagonal under Sym2.mk has cardinality (#s).choose 2.
Русский
Образ вне диагонали под отображением Sym2.mk имеет кардинал (#s).choose 2.
LaTeX
$$$|\mathrm{image}(\mathrm{Sym2.mk})\; s.offDiag| = \#s.select(2)$$$
Lean4
/-- The `offDiag` of `s : Finset α` is sent on a finset of `Sym2 α` of card `#s.offDiag / 2`.
This is because every element `s(x, y)` of `Sym2 α` not on the diagonal comes from exactly two
pairs: `(x, y)` and `(y, x)`. -/
theorem card_image_offDiag (s : Finset α) : #(s.offDiag.image Sym2.mk) = (#s).choose 2 := by
rw [Nat.choose_two_right, Nat.mul_sub_left_distrib, mul_one, ← offDiag_card,
Nat.div_eq_of_eq_mul_right Nat.zero_lt_two (two_mul_card_image_offDiag s).symm]
