dens_cons — Mathlib

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]

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