mathlib documentation

logic.unique

source
@[ext, class]
structure unique (α : Sort u) :
Sort (max 1 u)

Instances
source
theorem unique.ext_iff {α : Sort u} (x y : unique α) :
x = y ↔ x.to_inhabited = y.to_inhabited

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

source
@[instance]
def punit.unique  :
unique punit

Equations
source
@[instance]
def fin.unique  :
unique (fin 1)

Equations
source
@[instance]
def unique.inhabited {α : Sort u} [unique α] :
inhabited α

Equations
source
theorem unique.eq_default {α : Sort u} [unique α] (a : α) :
a = default α

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

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

source
theorem unique.forall_iff {α : Sort u} [unique α] {p : α → Prop} :
(∀ (a : α), p a) ↔ p (default α)

source
theorem unique.exists_iff {α : Sort u} [unique α] {p : α → Prop} :
Exists p ↔ p (default α)

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

source
@[instance]
def unique.subsingleton_unique {α : Sort u} :
subsingleton (unique α)

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

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

Equations
source
theorem function.injective.comap_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.

source
theorem nonempty_unique_or_exists_ne {α : Sort u} (x : α) :
nonempty (unique α) ∨ ∃ (y : α), y ≠ x

source
theorem subsingleton_or_exists_ne {α : Sort u} (x : α) :
subsingleton α ∨ ∃ (y : α), y ≠ x