English
Adding a new element to a Finset increases density by 1/|α| when the element was not present.
Русский
Добавление нового элемента в Finset увеличивает плотность на 1/|α|, если элемента ещё не было.
LaTeX
$$$\\text{If } a \\notin s,\\; \\mathrm{dens}(s\\cup\\{a\\}) = \\mathrm{dens}(s) + (|\\alpha|)^{-1}$$$
Lean4
@[simp]
theorem dens_cons (h : a ∉ s) : (s.cons a h).dens = dens s + (Fintype.card α : ℚ≥0)⁻¹ := by simp [dens, add_div]