English
The product of the ambient cardinality with the density equals the finitary cardinality of the set.
Русский
Произведение кардинальности окружающего типа на плотность равно кардинальности множества.
LaTeX
$$$\\mathrm{card}(\\alpha) \\cdot \\mathrm{dens}(s) = |s|$$$
Lean4
@[simp]
theorem card_mul_dens (s : Finset α) : Fintype.card α * s.dens = s.card :=
by
cases isEmpty_or_nonempty α
· simp [Subsingleton.elim s ∅]
rw [dens, mul_div_cancel₀]
exact mod_cast Fintype.card_ne_zero