# Documentation

Mathlib.Logic.Unique

# Types with a unique term #

In this file we define a typeclass Unique, which expresses that a type has a unique term. In other words, a type that is Inhabited and a Subsingleton.

## Main declaration #

• Unique: a typeclass that expresses that a type has a unique term.

## Main statements #

• Unique.mk': an inhabited subsingleton type is Unique. This can not be an instance because it would lead to loops in typeclass inference.

• Function.Surjective.unique: if the domain of a surjective function is Unique, then its codomain is Unique as well.

• Function.Injective.subsingleton: if the codomain of an injective function is Subsingleton, then its domain is Subsingleton as well.

• Function.Injective.unique: if the codomain of an injective function is Subsingleton and its domain is Inhabited, then its domain is Unique.

## Implementation details #

The typeclass Unique α is implemented as a type, rather than a Prop-valued predicate, for good definitional properties of the default term.

theorem Unique.ext {α : Sort u} (x : ) (y : ) (default : default = default) :
x = y
theorem Unique.ext_iff {α : Sort u} (x : ) (y : ) :
x = y default = default
class Unique (α : Sort u) extends :
Sort (max 1 u)
• default : α
• uniq : ∀ (a : α), a = default

In a Unique type, every term is equal to the default element (from Inhabited).

Unique α expresses that α is a type with a unique term default.

This is implemented as a type, rather than a Prop-valued predicate, for good definitional properties of the default term.

Instances
theorem unique_iff_exists_unique (α : Sort u) :
Nonempty () ∃! x, True
theorem unique_subtype_iff_exists_unique {α : Sort u_1} (p : αProp) :
Nonempty (Unique ()) ∃! a, p a
@[reducible]
def uniqueOfSubsingleton {α : Sort u_1} [] (a : α) :

Given an explicit a : α with Subsingleton α, we can construct a Unique α instance. This is a def because the typeclass search cannot arbitrarily invent the a : α term. Nevertheless, these instances are all equivalent by Unique.Subsingleton.unique.

See note [reducible non-instances].

Instances For
@[simp]
def uniqueProp {p : Prop} (h : p) :

Every provable proposition is unique, as all proofs are equal.

Instances For
theorem Fin.eq_zero (n : Fin 1) :
n = 0
instance inhabitedFinOneAdd (n : ) :
Inhabited (Fin (1 + n))
@[simp]
theorem Fin.default_eq_zero (n : ) :
default = 0
instance Unique.instInhabited {α : Sort u_1} [] :
theorem Unique.eq_default {α : Sort u_1} [] (a : α) :
a = default
theorem Unique.default_eq {α : Sort u_1} [] (a : α) :
default = a
instance Unique.instSubsingleton {α : Sort u_1} [] :
theorem Unique.forall_iff {α : Sort u_1} [] {p : αProp} :
((a : α) → p a) p default
theorem Unique.exists_iff {α : Sort u_1} [] {p : αProp} :
p default
theorem Unique.subsingleton_unique' {α : Sort u_1} (h₁ : ) (h₂ : ) :
h₁ = h₂
@[reducible]
def Unique.mk' (α : Sort u) [h₁ : ] [] :

Construct Unique from Inhabited and Subsingleton. Making this an instance would create a loop in the class inheritance graph.

Instances For
@[simp]
theorem Pi.default_def {α : Sort u_1} {β : αSort v} [(a : α) → Inhabited (β a)] :
default = fun a => default
theorem Pi.default_apply {α : Sort u_1} {β : αSort v} [(a : α) → Inhabited (β a)] (a : α) :
default ((a : α) → β a) () a = default
instance Pi.unique {α : Sort u_1} {β : αSort v} [(a : α) → Unique (β a)] :
Unique ((a : α) → β a)
instance Pi.uniqueOfIsEmpty {α : Sort u_1} [] (β : αSort v) :
Unique ((a : α) → β a)

There is a unique function on an empty domain.

theorem eq_const_of_subsingleton {α : Sort u_1} {β : Sort u_2} [] (f : αβ) (a : α) :
f = Function.const α (f a)
theorem eq_const_of_unique {α : Sort u_1} {β : Sort u_2} [] (f : αβ) :
f = Function.const α (f default)
theorem heq_const_of_unique {α : Sort u_1} [] {β : αSort v} (f : (a : α) → β a) :
HEq f (Function.const α (f default))
theorem Function.Injective.subsingleton {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) [] :

If the codomain of an injective function is a subsingleton, then the domain is a subsingleton as well.

theorem Function.Surjective.subsingleton {α : Sort u_1} {β : Sort u_2} {f : αβ} [] (hf : ) :

If the domain of a surjective function is a subsingleton, then the codomain is a subsingleton as well.

def Function.Surjective.unique {α : Sort u} {β : Sort u_1} (f : αβ) (hf : ) [] :

If the domain of a surjective function is a singleton, then the codomain is a singleton as well.

Instances For
def Function.Injective.unique {α : Sort u_1} {β : Sort u_2} {f : αβ} [] [] (hf : ) :

If α is inhabited and admits an injective map to a subsingleton type, then α is Unique.

Instances For
def Function.Surjective.uniqueOfSurjectiveConst (α : Type u_1) {β : Type u_2} (b : β) (h : ) :

If a constant function is surjective, then the codomain is a singleton.

Instances For
theorem Unique.bijective {A : Sort u_1} {B : Sort u_2} [] [] {f : AB} :

Option α is a Subsingleton if and only if α is empty.

instance Option.instUniqueOption {α : Type u_1} [] :
instance Unique.subtypeEq {α : Sort u} (y : α) :
Unique { x // x = y }
instance Unique.subtypeEq' {α : Sort u} (y : α) :
Unique { x // y = x }