singleton_one

Mathlib.Algebra.Group.Pointwise.Set.Basic

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

English

The image of the unit set under the singleton operation is the singleton set {1}.

Русский

Образ единичного множества под отображением равенству определяется единичным множеством {1}.

LaTeX

$$$1.{\\text{image}} \\!\\text{on} \\\\text{Set} = {1}$$$

Lean4

@[to_additive]
theorem singleton_one : ({ 1 } : Set α) = 1 :=
  rfl

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

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

Разделы

Аффилиация

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