dens_mul_card

Mathlib.Data.Finset.Density

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

English

Density times ambient cardinality equals the finset cardinality.

Русский

Плотность умноженная на кардинальность пространства равна кардинальности множества.

LaTeX

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

Lean4

@[simp]
theorem dens_mul_card (s : Finset α) : s.dens * Fintype.card α = s.card := by rw [mul_comm, card_mul_dens]

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

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

Разделы

Аффилиация

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