In classical mathematics, a subsingleton could either be defined as
a set $S$ such that for all elements $a \in S$ and $b \in S$, $a = b$
However, in constructive mathematics, the two notions of subsingleton above are no longer the same, because the axiom of excluded middle no longer holds true. Instead, one usually defines a subsingleton as the first definition, and the second definition is then referred to as about decidable subsingletons.
Similarly, in classical mathematics, an injection between two sets $A$ and $B$ is then a function $f:A \to B$ such that for all elements $b \in B$, the preimage or fiber of $f$ at $b$ is a subsingleton. However, in constructive mathematics, there are two notions of injections, resulting from the two notions of subsingletons:
An injection between two sets $A$ and $B$ is a function $f:A \to B$ such that for all elements $b \in B$, the preimage or fiber of $f$ at $b$ is a subsingleton.
A decidable injection between two sets $A$ and $B$ is a function $f:A \to B$ such that for all elements $b \in B$, the preimage or fiber of $f$ at $b$ is a decidable subsingleton; i.e. either empty or a singleton.
Suppose the set theory has function sets $B^A$. Then one could define the set of decidable injections from $A$ to $B$ as the set
where $f^*(b)$ is the preimage or fiber of $f$ at $b$.
Last revised on August 2, 2023 at 19:03:16. See the history of this page for a list of all contributions to it.