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 #

Main statements #

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 : Unique α) (y : Unique α) (default : default = default) :
x = y
theorem Unique.ext_iff {α : Sort u} (x : Unique α) (y : Unique α) :
x = y default = default
class Unique (α : Sort u) extends Inhabited :
Sort (max1u)
  • In a Unique type, every term is equal to the default element (from Inhabited).

    uniq : ∀ (a : α), a = 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
    theorem unique_subtype_iff_exists_unique {α : Sort u_1} (p : αProp) :
    Nonempty (Unique (Subtype p)) ∃! a, p a
    def uniqueOfSubsingleton {α : Sort u_1} [inst : 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
    Equations
    def uniqueProp {p : Prop} (h : p) :

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

    Equations
    • uniqueProp h = { toInhabited := { default := h }, uniq := (_ : ∀ (x : p), x = x) }
    theorem Fin.eq_zero (n : Fin 1) :
    n = 0
    Equations
    • instInhabitedFinSucc = { default := 0 }
    instance inhabitedFinOneAdd (n : ) :
    Inhabited (Fin (1 + n))
    Equations
    @[simp]
    theorem Fin.default_eq_zero (n : ) :
    default = 0
    instance Fin.unique :
    Equations
    instance Unique.instInhabited {α : Sort u_1} [inst : Unique α] :
    Equations
    • Unique.instInhabited = inst.toInhabited
    theorem Unique.eq_default {α : Sort u_1} [inst : Unique α] (a : α) :
    a = default
    theorem Unique.default_eq {α : Sort u_1} [inst : Unique α] (a : α) :
    default = a
    theorem Unique.forall_iff {α : Sort u_1} [inst : Unique α] {p : αProp} :
    ((a : α) → p a) p default
    theorem Unique.exists_iff {α : Sort u_1} [inst : Unique α] {p : αProp} :
    Exists p p default
    theorem Unique.subsingleton_unique' {α : Sort u_1} (h₁ : Unique α) (h₂ : Unique α) :
    h₁ = h₂
    def Unique.mk' (α : Sort u) [h₁ : Inhabited α] [inst : Subsingleton α] :

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

    Equations
    • Unique.mk' α = { toInhabited := { default := default }, uniq := (_ : ∀ (x : α), x = default) }
    @[simp]
    theorem Pi.default_def {α : Sort u_1} {β : αSort v} [inst : (a : α) → Inhabited (β a)] :
    default = fun a => default
    theorem Pi.default_apply {α : Sort u_1} {β : αSort v} [inst : (a : α) → Inhabited (β a)] (a : α) :
    default ((a : α) → β a) (instInhabitedForAll_1 α) a = default
    instance Pi.unique {α : Sort u_1} {β : αSort v} [inst : (a : α) → Unique (β a)] :
    Unique ((a : α) → β a)
    Equations
    instance Pi.uniqueOfIsEmpty {α : Sort u_1} [inst : IsEmpty α] (β : αSort v) :
    Unique ((a : α) → β a)

    There is a unique function on an empty domain.

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

    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 : αβ} [inst : Subsingleton α] (hf : Function.Surjective f) :

    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 : Function.Surjective f) [inst : Unique α] :

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

    Equations
    def Function.Injective.unique {α : Sort u_1} {β : Sort u_2} {f : αβ} [inst : Inhabited α] [inst : Subsingleton β] (hf : Function.Injective f) :

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

    Equations

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

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

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

    instance Option.instUniqueOption {α : Type u_1} [inst : IsEmpty α] :
    Equations
    instance Unique.subtypeEq {α : Sort u} (y : α) :
    Unique { x // x = y }
    Equations
    • Unique.subtypeEq y = { toInhabited := { default := { val := y, property := (_ : y = y) } }, uniq := (_ : ∀ (x : { x // x = y }), x = default) }
    instance Unique.subtypeEq' {α : Sort u} (y : α) :
    Unique { x // y = x }
    Equations
    • Unique.subtypeEq' y = { toInhabited := { default := { val := y, property := (_ : y = y) } }, uniq := (_ : ∀ (x : { x // y = x }), x = default) }