The Cantor-Schröder-Bernstein property

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 A is a part of B, and B is a part of A, then A is the same as B.

This can be seen in many settings. Most famously, it is a theorem of classical set theory when

• "A is a part of B" := there is an injection A \hookrightarrow B
• "A is the same as B" := there is a bijection A \xrightarrow{\cong} B

In classical set theory

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 f : A \hookrightarrow B and g : B \hookrightarrow A, then A \cong B.

That is: if two sets can be injectively mapped into each other, then there is a bijection between them.

Proof with choice

Please expand.

Proof without choice

Please expand.

Invalid constructively

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. \mathbf{Set}^{\to}).

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.

References

• 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:

• The Cantor-Bernstein theorem also holds for arbitrary types in HoTT with excluded middle: