powersetCard_empty_subsingleton

Mathlib.Data.Finset.Powerset

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

← MathLib Explorer

English

For all n, the set powersetCard(n, ∅) is subsingleton.

Русский

Для любого n множество powersetCard(n, ∅) является subsingleton.

LaTeX

$$powersetCard n ∅ .toSet . Subsingleton$$

Lean4

theorem powersetCard_empty_subsingleton (n : ℕ) : (powersetCard n (∅ : Finset α) : Set <| Finset α).Subsingleton := by
  simp [Set.Subsingleton, subset_empty]

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

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

Разделы

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

Аффилиация

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