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.10.0.tar.gz
md5=80dc98ed34340e31be9385fcd655e50d
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: 07 Dec 2019
On This Page