dens_singleton

Mathlib.Data.Finset.Density

URI: https://scilib.ai/kg/mathlib#Finset.dens_singleton

English

The density of a singleton is the reciprocal of the ambient cardinality.

Русский

Плотность одиночного множества равна обратному значению кардинальности пространства.

LaTeX

$$$\\mathrm{dens}({a}) = (|\\alpha|)^{-1}$$$

Lean4

@[simp]
theorem dens_singleton (a : α) : dens ({ a } : Finset α) = (Fintype.card α : ℚ≥0)⁻¹ := by simp [dens]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru