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.7.0.tar.gz
md5=e45808e361e73cfd09dfad9ed47a47a6
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: 11 Jan 2019
On This Page