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.

class Unique (α : Sort u) extends Inhabited α :
Sort (max 1 u)

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.ext_iff {α : Sort u} {x y : Unique α} :
    theorem Unique.ext {α : Sort u} {x y : Unique α} (default : default = default) :
    x = y
    @[deprecated unique_iff_existsUnique (since := "2024-12-17")]

    Alias of unique_iff_existsUnique.

    theorem unique_subtype_iff_existsUnique {α : Sort u_1} (p : αProp) :
    Nonempty (Unique (Subtype p)) ∃! a : α, p a
    @[deprecated unique_subtype_iff_existsUnique (since := "2024-12-17")]
    theorem unique_subtype_iff_exists_unique {α : Sort u_1} (p : αProp) :
    Nonempty (Unique (Subtype p)) ∃! a : α, p a

    Alias of unique_subtype_iff_existsUnique.

    @[reducible, inline]
    abbrev uniqueOfSubsingleton {α : 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
      Instances For
        def uniqueProp {p : Prop} (h : p) :

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

        Equations
          Instances For
            Equations
              @[instance 100]
              instance Unique.instInhabited {α : Sort u_1} [Unique α] :
              Equations
                theorem Unique.eq_default {α : Sort u_1} [Unique α] (a : α) :
                theorem Unique.default_eq {α : Sort u_1} [Unique α] (a : α) :
                @[instance 100]
                instance Unique.instSubsingleton {α : Sort u_1} [Unique α] :
                theorem Unique.forall_iff {α : Sort u_1} [Unique α] {p : αProp} :
                (∀ (a : α), p a) p default
                theorem Unique.exists_iff {α : Sort u_1} [Unique α] {p : αProp} :
                theorem Unique.subsingleton_unique' {α : Sort u_1} (h₁ h₂ : Unique α) :
                h₁ = h₂
                theorem Unique.subsingleton_unique'_iff {α : Sort u_1} {h₁ h₂ : Unique α} :
                h₁ = h₂ True
                @[reducible, inline]
                abbrev 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
                  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 : α) :
                    instance Pi.unique {α : Sort u_1} {β : αSort v} [(a : α) → Unique (β a)] :
                    Unique ((a : α) → β a)
                    Equations
                      instance Pi.uniqueOfIsEmpty {α : Sort u_1} [IsEmpty α] (β : αSort v) :
                      Unique ((a : α) → β a)

                      There is a unique function on an empty domain.

                      Equations
                        theorem eq_const_of_subsingleton {α : Sort u_1} {β : Sort u_2} [Subsingleton α] (f : αβ) (a : α) :
                        f = Function.const α (f a)
                        theorem eq_const_of_unique {α : Sort u_1} {β : Sort u_2} [Unique α] (f : αβ) :
                        theorem heq_const_of_unique {α : Sort u_1} [Unique α] {β : αSort v} (f : (a : α) → β a) :
                        theorem Function.Injective.subsingleton {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : Injective f) [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 : αβ} [Subsingleton α] (hf : 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_2} {α : Sort u} (f : αβ) (hf : Surjective f) [Unique α] :

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

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

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

                            Equations
                              Instances For
                                def Function.Surjective.uniqueOfSurjectiveConst (α : Type u_3) {β : Type u_4} (b : β) (h : Surjective (const α b)) :

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

                                Equations
                                  Instances For
                                    def uniqueElim {ι : Sort u_2} {α : ιSort u_3} [Unique ι] (x : α default) (i : ι) :
                                    α i

                                    Given one value over a unique, we get a dependent function.

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem uniqueElim_default {ι : Sort u_2} {α : ιSort u_3} {x✝ : Unique ι} (x : α default) :
                                        @[simp]
                                        theorem uniqueElim_const {ι : Sort u_2} {β : Sort u_4} {x✝ : Unique ι} (x : β) (i : ι) :
                                        theorem Unique.bijective {A : Sort u_2} {B : Sort u_3} [Unique A] [Unique B] {f : AB} :

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

                                        instance Option.instUniqueOfIsEmpty {α : Type u_2} [IsEmpty α] :
                                        Equations
                                          instance Unique.subtypeEq {α : Sort u_1} (y : α) :
                                          Unique { x : α // x = y }
                                          Equations
                                            instance Unique.subtypeEq' {α : Sort u_1} (y : α) :
                                            Unique { x : α // y = x }
                                            Equations
                                              instance Fin.instUnique :
                                              Equations