Power sets, orders, cardinality over infinite sets. Includes functional and relational facts based on Axiom of Choice and refinement relations based on equivalence relations.
| Theorem | Location | PVS Name | Contributors |
|---|---|---|---|
| Denumerability of the Rational Numbers | sets_aux@countable_set |
countable_rat |
Jerry James |
- Bruno Dutertre, SRI, USA
- David Lester, Manchester University, UK
- Jerry James, Utah State University, USA
- Dragan Stosic, Ireland
- Jon Sjogren, Department of Defense, USA
- Ricky Butler, NASA, USA
- Anthony Narkawicz, NASA, USA
- César Muñoz, NASA, USA
- Sam Owre, SRI, USA
- Marco A. Feliú, NIA & NASA, USA
- Mariano Moscato, NIA & NASA, USA
- César Muñoz, NASA, USA
