powerset_empty

Mathlib.Data.Finset.Powerset

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

English

The powerset of the empty set is the singleton set containing the empty set.

Русский

Множество подмножеств пустого множества равно единичному множеству, содержающему пустое множество.

LaTeX

$$$$ (\\emptyset).powerset = \\{\\emptyset\\}. $$$$

Lean4

@[simp]
theorem powerset_empty : (∅ : Finset α).powerset = {∅} :=
  rfl

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

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

Разделы

Аффилиация

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