Theorems · Definition · logic and foundations

Equiv.Set.singleton

{α : Type u_3} → (a : α) → ↑{a} ≃ PUnit.{u}

A singleton set is equivalent to a PUnit type.

Defined in

Mathlib.Logic.Equiv.Set

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms