singleton

Mathlib.Logic.Equiv.Set

URI: https://scilib.ai/kg/mathlib#Equiv.Set.singleton

← MathLib Explorer

English

A singleton set {a} is equivalent to the unit type PUnit.

Русский

Единичное множество {a} эквивалентно типу PUnit.

LaTeX

$$({a} : Set α) ≃ PUnit$$

Lean4

/-- A singleton set is equivalent to a `PUnit` type. -/
protected def singleton {α} (a : α) : ({ a } : Set α) ≃ PUnit.{u} :=
  ⟨fun _ => PUnit.unit, fun _ => ⟨a, mem_singleton _⟩, fun ⟨x, h⟩ =>
    by
    subst x
    rfl, fun ⟨⟩ => rfl⟩

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

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

Разделы

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

Аффилиация

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