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_iff {α : Sort u} {x : Unique α} {y : Unique α} :
x = y default = default
theorem Unique.ext {α : Sort u} {x : Unique α} {y : Unique α} (default : Inhabited.default = Inhabited.default) :
x = y
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.

  • default : α
  • uniq : ∀ (a : α), a = default

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

Instances
    theorem Unique.uniq {α : Sort u} (self : Unique α) (a : α) :
    a = default

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

    theorem unique_iff_exists_unique (α : Sort u) :
    Nonempty (Unique α) ∃! x : α, True
    theorem unique_subtype_iff_exists_unique {α : Sort u_1} (p : αProp) :
    Nonempty (Unique (Subtype p)) ∃! a : α, p a
    @[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
      @[simp]
      def uniqueProp {p : Prop} (h : p) :

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

      Equations
      Instances For
        @[instance 100]
        instance Unique.instInhabited {α : Sort u_1} [Unique α] :
        Equations
        • Unique.instInhabited = inst.toInhabited
        theorem Unique.eq_default {α : Sort u_1} [Unique α] (a : α) :
        a = default
        theorem Unique.default_eq {α : Sort u_1} [Unique α] (a : α) :
        default = a
        @[instance 100]
        instance Unique.instSubsingleton {α : Sort u_1} [Unique α] :
        Equations
        • =
        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} :
        Exists p p default
        theorem Unique.subsingleton_unique'_iff {α : Sort u_1} {h₁ : Unique α} {h₂ : Unique α} :
        h₁ = h₂ True
        theorem Unique.subsingleton_unique' {α : Sort u_1} (h₁ : Unique α) (h₂ : Unique α) :
        h₁ = h₂
        Equations
        • =
        @[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 : α) :
          default a = default
          instance Pi.unique {α : Sort u_1} {β : αSort v} [(a : α) → Unique (β a)] :
          Unique ((a : α) → β a)
          Equations
          • Pi.unique = { toInhabited := Pi.instInhabited, uniq := }
          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 : αβ) :
          f = Function.const α (f default)
          theorem heq_const_of_unique {α : Sort u_1} [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) [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 : 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_2} {α : Sort u} (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
          Instances For
            def Function.Injective.unique {α : Sort u_1} {β : Sort u_2} {f : αβ} [Inhabited α] [Subsingleton β] (hf : Function.Injective f) :

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

            Equations
            Instances For

              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_1 : α default), uniqueElim x_1 default = x_1
                  @[simp]
                  theorem uniqueElim_const {ι : Sort u_2} {β : Sort u_4} :
                  ∀ {x : Unique ι} (x_1 : β) (i : ι), uniqueElim x_1 i = x_1
                  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