@[instance]
Equations
- punit.unique = {to_inhabited := {default := punit.star}, uniq := punit.unique._proof_1}
@[instance]
Equations
- fin.unique = {to_inhabited := {default := 0}, uniq := fin.unique._proof_1}
@[instance]
Equations
- unique.inhabited = _inst_1.to_inhabited
@[instance]
Equations
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 α)
@[instance]
Equations
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
- hf.unique = {to_inhabited := {default := f (inhabited.default α)}, uniq := _}
theorem
function.injective.comap_subsingleton
{α : Sort u}
{β : Sort v}
{f : α → β}
(hf : function.injective f)
[subsingleton β] :
If the codomain of an injective function is a subsingleton, then the domain is a subsingleton as well.