Contribution: Schroeder
The Theorem of Schroeder-Bernstein
Authors
- Hugo herbelin
Description
Fraenkel's proof of Schroeder-Bernstein theorem on decidable sets is formalized in a constructive variant of set theory based on stratified universes (the one defined in the Ensemble library). The informal proof can be found for instance in "Axiomatic Set Theory" from P. Suppes.
Keywords
schroeder bernstein, set theory