singleton_def

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Set.singleton_def

English

The singleton {a} is equal to inserting a into the empty set: {a} = insert a ∅.

Русский

Одиночное множество {a} равно вставке a в пустое множество: {a} = insert a ∅.

LaTeX

$$$\{a\} = \operatorname{insert} (a) \emptyset$$$

Lean4

theorem singleton_def (a : α) : ({ a } : Set α) = insert a ∅ :=
  (insert_empty_eq a).symm

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

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

Разделы

Аффилиация

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