card_mul_dens — Mathlib

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

Похожие утверждения