dens — Mathlib

English

Density of a finset s is the fraction of elements of s in the ambient type α, i.e., |s| / |α|.

Русский

Плотность множества s равна отношению числа элементов s к размеру пространства α: |s|/|α|.

LaTeX

$$$\\mathrm{dens}(s) = \\dfrac{|s|}{|\\alpha|}$$$

Lean4

/-- Density of a finset.

`dens s` is the number of elements of `s` divided by the size of the ambient type `α`. -/
def dens (s : Finset α) : ℚ≥0 :=
  s.card / Fintype.card α

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