package coq-schroeder
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
The Theorem of Schroeder-Bernstein
Install
Dune Dependency
Authors
Maintainers
Sources
v8.8.0.tar.gz
md5=f9dd55ccc87a31322bb33fc9e7f80254
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.
Tags
keyword: Schroeder-Bernstein keyword: set theory category: Mathematics/Logic/Set theoryPublished: 06 Feb 2019
On This Page