mem_powersetCard_univ

Mathlib.Data.Fintype.Powerset

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

English

For any k, s ∈ powersetCard k univ iff |s| = k.

Русский

Для любого k, s принадлежит powersetCard k univ тогда, когда |s| = k.

LaTeX

$$$s \\in \\mathrm{powersetCard}\\,k\\, (\\mathrm{univ}) \\iff |s| = k$$$

Lean4

theorem mem_powersetCard_univ : s ∈ powersetCard k (univ : Finset α) ↔ #s = k :=
  mem_powersetCard.trans <| and_iff_right <| subset_univ _

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

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

Разделы

Аффилиация

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