mathlib3 documentation

logic.unique

Types with a unique term #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[ext, class]

structure unique (α : Sort u) :

Sort (max 1 u)

to_inhabited : inhabited α
uniq : ∀ (a : α), a = inhabited.default

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 of this typeclass

Instances of other typeclasses for unique

unique.has_sizeof_inst
unique.subsingleton_unique

theorem unique.ext_iff {α : Sort u} (x y : unique α) :

x = y ↔ x.to_inhabited = y.to_inhabited

theorem unique.ext {α : Sort u} (x y : unique α) (h : x.to_inhabited = y.to_inhabited) :

x = y

theorem unique_iff_exists_unique (α : Sort u) :

nonempty (unique α) ↔ ∃! (a : α), true

theorem unique_subtype_iff_exists_unique {α : Sort u_1} (p : α → Prop) :

nonempty (unique (subtype p)) ↔ ∃! (a : α), p a

@[reducible]

def unique_of_subsingleton {α : Sort u_1} [subsingleton α] (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].

Equations

unique_of_subsingleton a = {to_inhabited := {default := a}, uniq := _}

@[protected, instance]

def punit.unique :

Equations

punit.unique = {to_inhabited := {default := punit.star}, uniq := punit.unique._proof_1}

@[simp]

theorem punit.default_eq_star :

inhabited.default = punit.star

def unique_prop {p : Prop} (h : p) :

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

Equations

unique_prop h = {to_inhabited := {default := h}, uniq := _}

@[protected, instance]

def true.unique :

Equations

true.unique = unique_prop trivial

theorem fin.eq_zero (n : fin 1) :

n = 0

@[protected, instance]

def fin.inhabited {n : ℕ} :

inhabited (fin n.succ)

Equations

fin.inhabited = {default := 0}

@[protected, instance]

def inhabited_fin_one_add (n : ℕ) :

inhabited (fin (1 + n))

Equations

inhabited_fin_one_add n = {default := ⟨0, _⟩}

@[simp]

theorem fin.default_eq_zero (n : ℕ) :

inhabited.default = 0

@[protected, instance]

def fin.unique :

Equations

fin.unique = {to_inhabited := {default := inhabited.default fin.inhabited}, uniq := fin.eq_zero}

@[protected, instance]

def unique.inhabited {α : Sort u} [unique α] :

Equations

unique.inhabited = _inst_1.to_inhabited

theorem unique.eq_default {α : Sort u} [unique α] (a : α) :

a = inhabited.default

theorem unique.default_eq {α : Sort u} [unique α] (a : α) :

inhabited.default = a

@[protected, instance]

def unique.subsingleton {α : Sort u} [unique α] :

subsingleton α

theorem unique.forall_iff {α : Sort u} [unique α] {p : α → Prop} :

(∀ (a : α), p a) ↔ p inhabited.default

theorem unique.exists_iff {α : Sort u} [unique α] {p : α → Prop} :

Exists p ↔ p inhabited.default

@[protected, ext]

theorem unique.subsingleton_unique' {α : Sort u} (h₁ h₂ : unique α) :

h₁ = h₂

@[protected, instance]

def unique.subsingleton_unique {α : Sort u} :

subsingleton (unique α)

@[reducible]

def unique.mk' (α : Sort u) [h₁ : inhabited α] [subsingleton α] :

Construct unique from inhabited and subsingleton. Making this an instance would create a loop in the class inheritance graph.

Equations

unique.mk' α = {to_inhabited := {default := inhabited.default h₁}, uniq := _}

theorem unique_iff_subsingleton_and_nonempty (α : Sort u) :

nonempty (unique α) ↔ subsingleton α ∧ nonempty α

@[simp]

theorem pi.default_def {α : Sort u} {β : α → Sort v} [Π (a : α), inhabited (β a)] :

inhabited.default = λ (a : α), inhabited.default

theorem pi.default_apply {α : Sort u} {β : α → Sort v} [Π (a : α), inhabited (β a)] (a : α) :

inhabited.default a = inhabited.default

@[protected, instance]

def pi.unique {α : Sort u} {β : α → Sort v} [Π (a : α), unique (β a)] :

unique (Π (a : α), β a)

Equations

pi.unique = {to_inhabited := {default := inhabited.default (pi.inhabited α)}, uniq := _}

@[protected, instance]

def pi.unique_of_is_empty {α : Sort u} [is_empty α] (β : α → Sort v) :

unique (Π (a : α), β a)

There is a unique function on an empty domain.

Equations

pi.unique_of_is_empty β = {to_inhabited := {default := is_empty_elim (λ (a : α), β a)}, uniq := _}

theorem eq_const_of_unique {α : Sort u} {β : Sort v} [unique α] (f : α → β) :

f = function.const α (f inhabited.default)

theorem heq_const_of_unique {α : Sort u} [unique α] {β : α → Sort v} (f : Π (a : α), β a) :

f == function.const α (f inhabited.default)

@[protected]

theorem function.injective.subsingleton {α : Sort u} {β : Sort v} {f : α → β} (hf : function.injective f) [subsingleton β] :

subsingleton α

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

@[protected]

theorem function.surjective.subsingleton {α : Sort u} {β : Sort v} {f : α → β} [subsingleton α] (hf : function.surjective f) :

subsingleton β

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

@[protected]

def function.surjective.unique {α : Sort u} {β : Sort v} {f : α → β} (hf : function.surjective f) [unique α] :

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

Equations

hf.unique = unique.mk' β

@[protected]

def function.injective.unique {α : Sort u} {β : Sort v} {f : α → β} [inhabited α] [subsingleton β] (hf : function.injective f) :

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

Equations

hf.unique = unique.mk' α

def function.surjective.unique_of_surjective_const (α : Type u_1) {β : Type u_2} (b : β) (h : function.surjective (function.const α b)) :

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

Equations

function.surjective.unique_of_surjective_const α b h = unique_of_subsingleton b

theorem unique.bijective {A : Sort u_1} {B : Sort u_2} [unique A] [unique B] {f : A → B} :

function.bijective f

theorem option.subsingleton_iff_is_empty {α : Type u_1} :

subsingleton (option α) ↔ is_empty α

option α is a subsingleton if and only if α is empty.

@[protected, instance]

def option.unique {α : Type u_1} [is_empty α] :

unique (option α)

Equations

option.unique = unique.mk' (option α)

@[protected, instance]

def unique.subtype_eq {α : Sort u} (y : α) :

unique {x // x = y}

Equations

unique.subtype_eq y = {to_inhabited := {default := ⟨y, _⟩}, uniq := _}

@[protected, instance]

def unique.subtype_eq' {α : Sort u} (y : α) :

unique {x // y = x}

Equations

unique.subtype_eq' y = {to_inhabited := {default := ⟨y, _⟩}, uniq := _}