powersetCard_nonempty

Mathlib.Data.Finset.Powerset

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

← MathLib Explorer

English

The nonemptiness of powersetCard n s is equivalent to n ≤ |s|.

Русский

Непустота powersetCard n s эквивалентна n ≤ |s|.

LaTeX

$$(powersetCard n s).Nonempty ↔ n ≤ card s$$

Lean4

@[simp]
theorem powersetCard_nonempty : (powersetCard n s).Nonempty ↔ n ≤ s.card := by
  aesop (add simp [Finset.Nonempty, exists_subset_card_eq, card_le_card])

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

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

Разделы

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

Аффилиация

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