The Cantor-Schröder-Bernstein is the following property of mathematical objects, which is parameterized on the notions of "is a part of" and "is the same as."
Definition (Cantor-Schröder-Bernstein). If is a part of , and is a part of , then is the same as .
This can be seen in many settings. Most famously, it is a theorem of classical set theory when
The Cantor-Bernstein theorem (aka the Schröder–Bernstein theorem) is theorem of classical set theory.
Theorem (Cantor-Schröder-Bernstein). If there are injections and , then .
That is: if two sets can be injectively mapped into each other, then there is a bijection between them.
Please expand.
Please expand.
It is well-known that the CSB property does not hold in many constructive settings. For example, the nLab mentions that it holds in Boolean topoi, but not in other topoi (e.g. ).
Moreover, it is known that this goes the other way: the CSB property implies the law of the excluded middle in constructive set theory. This was shown by [Pradic and Brown 2019].
There is a Wikipedia and an nLab page on the Cantor-Schröder-Bernstein theorem.
In 2019 Pradic and Brown published a proof that the Cantor-Schröder-Bernstein property implies excluded middle:
Pradic, Pierre and Chad E. Brown. Cantor-Bernstein implies Excluded Middle. 2019. https://arxiv.org/abs/1904.09193
Escardó, M.H. The Cantor–Schröder–Bernstein Theorem for ∞-groupoids. Journal of Homotopy and Related Structures (2021). https://doi.org/10.1007/s40062-021-00284-6