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.9.0.tar.gz
md5=df101200f9232b0135b7ee345705e6ef
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