powersetCard_card_add

Mathlib.Data.Finset.Powerset

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

English

If n > 0, then powersetCard (|s| + n) s = ∅; there are no larger subsets of s.

Русский

Если n > 0, то powersetCard(|s|+n) s пусто; подпmножества размера больше |s| не существует.

LaTeX

$$powersetCard (s.card + n) s = ∅ (for 0 < n)$$

Lean4

@[simp]
theorem powersetCard_card_add (s : Finset α) (hn : 0 < n) : s.powersetCard (s.card + n) = ∅ := by simpa

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

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

Разделы

Аффилиация

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