存在唯一性证明

给出一个候选并验证它，只完成存在性；排除多解但未保证解存在，只完成唯一性。两个任务需要明确分开。

“存在唯一”包含两个逻辑上独立的任务：先证明至少有一个对象满足性质，再证明任意两个满足者必相等。仅构造一个候选不能排除其他候选，仅证明“至多一个”也不能保证对象存在。很多证明还把唯一性改写为某个规范映射单射，或把存在性改写为满射。

线性方程 $ax=b$ 在 $a\ne 0$ 时有唯一实解 $b/a$。常微分方程的存在唯一性定理需要连续性或 Lipschitz 等条件；去掉条件可能无解或多解。

对 $a>0$，方程 $x^2=a$ 在正实数中有唯一解。存在性可由实数完备性得到一个正平方根；唯一性则独立证明：若 $x,y>0$ 且 $x^2=y^2$，则

而 $x+y>0$，故 $x=y$。边界情形清楚显示两个部分彼此独立：若把范围扩大到全部实数，$a>0$ 时通常有两个解；若删掉 $a>0$，还可能无正实解。对象范围和假设同时参与“存在唯一”的结论。

逆函数、递归定义、规范形和商结构上的运算都需要存在唯一性。唯一性常通过假设两个候选并比较其满足的同一性质证明。

单射公理库单射Injective function · One-to-one function不同输入必有不同输出的函数。表达至多一个原像，满射公理库满射Surjective function · Onto function陪域中每个元素都有至少一个原像的函数。表达至少一个原像，二者合成双射。泛性质公理库泛性质Universal property在候选结构组成的范畴中以始对象或终对象刻画构造。中的唯一分解、常微分方程初值问题和递归定义都采用存在加唯一的双重结构。