powersetCard_eq_empty

Mathlib.Data.Finset.Powerset

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

← MathLib Explorer

English

PowersetCard n s equals empty iff card s < n.

Русский

PowersetCard n s пусто тогда, когда |s| < n.

LaTeX

$$powersetCard n s = ∅ ↔ card s < n$$

Lean4

@[simp]
theorem powersetCard_eq_empty : powersetCard n s = ∅ ↔ s.card < n :=
  by
  refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩
  contrapose!
  exact fun h ↦ nonempty_iff_ne_empty.1 <| (exists_subset_card_eq h).imp <| by simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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