univ_filter_card_eq

Mathlib.Data.Fintype.Powerset

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

English

For a finite α, the set of all subsets of size k equals univ.powersetCard k.

Русский

Для конечного α множество всех подмножеств размера k равно univ.powersetCard k.

LaTeX

$$$\\{ s : Finset(\\alpha) \\mid |s| = k \\} = \\mathrm{univ}.\\mathrm{powersetCard} k$$$

Lean4

@[simp]
theorem univ_filter_card_eq (k : ℕ) : ({s | #s = k} : Finset (Finset α)) = univ.powersetCard k := by ext; simp

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

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

Разделы

Аффилиация

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