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.6.0.tar.gz
md5=ddca334912fb99be950a0adc39a09c2d
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: 20 Nov 2018
On This Page